Changeset 849 for src/ASM


Ignore:
Timestamp:
May 26, 2011, 6:41:33 PM (10 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r848 r849  
    199199 ∀A:Type[0].∀l,l1,l2:list A.
    200200  is_prefix … l l1 → is_prefix … l (l1@l2).
     201
     202record Propify (A:Type[0]) : Prop ≝ { in_propify: A }.
     203
     204definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
     205 λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
     206
     207let rec foldli (A: Type[0]) (B: Type[0]) (f: Propify nat → A → B → A) (i: Propify nat) (a: A) (l: list B) on l ≝
     208  match l with
     209  [ nil ⇒ a
     210  | cons hd tl ⇒ foldli A B f (match i with [ mk_Propify i ⇒ mk_Propify … (S i)]) (f i a hd) tl
     211  ].
    201212
    202213definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.