Changeset 2440


Ignore:
Timestamp:
Nov 7, 2012, 5:11:41 PM (7 years ago)
Author:
piccolo
Message:

fixed range_strong and linearise
(commit by Paolo, he's to blame in case)

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2422 r2440  
    675675   (joint_if_stacksize ?? f_in)
    676676   (linearise_code p globals (joint_if_code … f_in) (pi2 … f_sig) (joint_if_entry … f_in))
    677    0 0 (* exit is dummy! *), ?».
     677   0 0 (* exit is dummy! *), ?». [2,4:// ]
    678678elim (linearise_code ?????) #c * #code_closed
    679679[3: #_ assumption ]
  • src/utilities/lists.ma

    r2314 r2440  
    150150definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
    151151// qed.
     152
     153let rec range_strong_internal (start, how_many, end : ℕ)
     154  on how_many : start + how_many ≤ end → list (Σn : ℕ.n < end) ≝
     155match 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/
     162qed.
     163
     164definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝
     165  λend.range_strong_internal 0 end end (le_n …).
    152166
    153167definition List ≝ MakeMonadProps
Note: See TracChangeset for help on using the changeset viewer.