Changeset 849


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

...

Location:
src
Files:
2 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' ≝
  • src/common/AST.ma

    r795 r849  
    179179}.
    180180
     181(*
    181182definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
    182183  map ?? (fst ident F) (prog_funct ?? p).
     
    496497(*
    497498End TRANSF_PARTIAL_FUNDEF.
     499*)
    498500*)
    499501
Note: See TracChangeset for help on using the changeset viewer.