Changeset 849 for src/ASM/AssemblyProof.ma

Timestamp:

May 26, 2011, 6:41:33 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -199 +199 @@
  ∀A:Type[0].∀l,l1,l2:list A.
   is_prefix … l l1 → is_prefix … l (l1@l2).
+
+record Propify (A:Type[0]) : Prop ≝ { in_propify: A }.
+
+definition Propify_elim: ∀A. ∀P:Prop. (A → P) → (Propify A → P) ≝
+ λA,P,H,x. match x with [ mk_Propify p ⇒ H p ].
+
+let rec foldli (A: Type[0]) (B: Type[0]) (f: Propify nat → A → B → A) (i: Propify nat) (a: A) (l: list B) on l ≝
+  match l with
+  [ nil ⇒ a
+  | cons hd tl ⇒ foldli A B f (match i with [ mk_Propify i ⇒ mk_Propify … (S i)]) (f i a hd) tl
+  ].
 
 definition build_maps' ≝