Changeset 1355 for src/common


Ignore:
Timestamp:
Oct 11, 2011, 3:32:15 PM (8 years ago)
Author:
sacerdot
Message:

monadic fold_lefti added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1351 r1355  
    173173Qed.
    174174*)
     175
     176(* A monadic fold_lefti *)
     177let 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
     186definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.
     187
    175188
    176189(* A monadic fold_left2 *)
Note: See TracChangeset for help on using the changeset viewer.