Changeset 1355

Timestamp:

Oct 11, 2011, 3:32:15 PM (9 years ago)

Author:

sacerdot

Message:

monadic fold_lefti added

File:

• src/common/Errors.ma (modified) (1 diff)

src/common/Errors.ma

@@ -173 +173 @@
 Qed.
 *)
+
+(* A monadic fold_lefti *)
+let rec mfold_left_i_aux (A: Type[0]) (B: Type[0])
+                        (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝
+  match l with
+    [ nil ⇒ x
+    | cons hd tl ⇒
+       do x ← x ;
+       mfold_left_i_aux A B f (f i x hd) (S i) tl
+    ].
+
+definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.
+
 
 (* A monadic fold_left2 *)