Changeset 1355
- Timestamp:
- Oct 11, 2011, 3:32:15 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Errors.ma
r1351 r1355 173 173 Qed. 174 174 *) 175 176 (* A monadic fold_lefti *) 177 let rec mfold_left_i_aux (A: Type[0]) (B: Type[0]) 178 (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝ 179 match l with 180 [ nil ⇒ x 181 | cons hd tl ⇒ 182 do x ← x ; 183 mfold_left_i_aux A B f (f i x hd) (S i) tl 184 ]. 185 186 definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O. 187 175 188 176 189 (* A monadic fold_left2 *)
Note: See TracChangeset
for help on using the changeset viewer.