Changeset 342 for Deliverables

Timestamp:

Nov 30, 2010, 4:46:45 PM (10 years ago)

Author:

sacerdot

Message:

fold_lefti

File:

• Deliverables/D4.1/Matita/List.ma (modified) (1 diff)

Deliverables/D4.1/Matita/List.ma

@@ -222 +222 @@
     | Cons hd tl ⇒ f (fold_left A B f x tl) hd
     ].
+
+nlet rec fold_lefti_aux (A: Type[0]) (B: Type[0])
+                   (f: Nat → A → B → A) (x: A) (i: Nat) (l: List B) on l ≝
+  match l with
+    [ Empty ⇒ x
+    | Cons hd tl ⇒ f i (fold_lefti_aux A B f x (S i) tl) hd
+    ].
+
+ndefinition fold_lefti ≝ λA,B,f,x. fold_lefti_aux A B f x Z.
     
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)