Changeset 1125 for src/common


Ignore:
Timestamp:
Aug 29, 2011, 3:07:15 PM (8 years ago)
Author:
sacerdot
Message:

Monadic mfold_left2 added.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r797 r1125  
    141141  constructor. auto. auto.
    142142Qed.
    143 
     143*)
     144
     145(* A monadic fold_left2 *)
     146
     147axiom WrongLength: String.
     148
     149let rec mfold_left2
     150  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
     151  (left: list B) (right: list C) on left: res A ≝
     152  match left with
     153  [ nil ⇒
     154    match right with
     155    [ nil ⇒ accu
     156    | cons hd tl ⇒ Error ? (msg WrongLength)
     157    ]
     158  | cons hd tl ⇒
     159    match right with
     160    [ nil ⇒ Error ? (msg WrongLength)
     161    | cons hd' tl' ⇒
     162       do accu ← accu;
     163       mfold_left2 … f (f accu hd hd') tl tl'
     164    ]
     165  ].
     166
     167(*
    144168(** * Reasoning over monadic computations *)
    145169
Note: See TracChangeset for help on using the changeset viewer.