Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/common/Errors.ma

    r1102 r1153  
    162162  constructor. auto. auto.
    163163Qed.
    164 
     164*)
     165
     166(* A monadic fold_left2 *)
     167
     168axiom WrongLength: String.
     169
     170let rec mfold_left2
     171  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
     172  (left: list B) (right: list C) on left: res A ≝
     173  match left with
     174  [ nil ⇒
     175    match right with
     176    [ nil ⇒ accu
     177    | cons hd tl ⇒ Error ? (msg WrongLength)
     178    ]
     179  | cons hd tl ⇒
     180    match right with
     181    [ nil ⇒ Error ? (msg WrongLength)
     182    | cons hd' tl' ⇒
     183       do accu ← accu;
     184       mfold_left2 … f (f accu hd hd') tl tl'
     185    ]
     186  ].
     187
     188(*
    165189(** * Reasoning over monadic computations *)
    166190
Note: See TracChangeset for help on using the changeset viewer.