Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (8 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/lists.ma

    r2440 r2443  
    150150definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
    151151// qed.
    152 
    153 let rec range_strong_internal (start, how_many, end : ℕ)
    154   on how_many : start + how_many ≤ end → list (Σn : ℕ.n < end) ≝
    155 match how_many return λx.start + x ≤ end → ?
    156   with
    157 [ O ⇒ λ_.[ ]
    158 | S k ⇒ λprf.«start, ?» :: range_strong_internal (S start) k end ?
    159 ].
    160 [2: //]
    161 >(plus_n_O start) /2 by plus_lt_to_lt/
    162 qed.
    163 
    164 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
    165   λend.range_strong_internal 0 end end (le_n …).
    166152
    167153definition List ≝ MakeMonadProps
     
    379365| cons h t ⇒ ordered_insert A lt h (insert_sort A lt t)
    380366].
     367
     368(* range from 0 to n excluded with proof of minoration *)
     369
     370let rec range_strong_internal (index, how_many, end : ℕ) on how_many :
     371  index + how_many = end →
     372  list (Σn.n<end) ≝
     373  match how_many return λhow_many.index + how_many = end → ? with
     374  [ O ⇒ λ_.[ ]
     375  | S k ⇒ λprf.«index, ?» :: range_strong_internal (S index) k end ?
     376  ].
     377<prf
     378[ >(plus_n_O index) in ⊢ (?%?); @monotonic_lt_plus_r @le_S_S @le_O_n
     379| @plus_n_Sm
     380]
     381qed.
     382
     383definition range_strong : ∀end.list (Σn.n < end) ≝
     384λend.range_strong_internal 0 ? end (refl …).
Note: See TracChangeset for help on using the changeset viewer.