Changeset 636 for Deliverables/D3.1/Csemantics/Errors.ma
 Timestamp:
 Mar 4, 2011, 6:20:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Errors.ma
r487 r636 16 16 include "basics/types.ma". 17 17 include "basics/logic.ma". 18 include "basics/list.ma". 18 19 19 20 (* * Error reporting and the error monad. *) … … 107 108 108 109 (** This is the familiar monadic map iterator. *) 109 110 Fixpoint mmap (A B: Type) (f: A > res B) (l: list A) {struct l} : res (list B) := 110 *) 111 112 let rec mmap (A, B: Type[0]) (f: A → res B) (l: list A) on l : res (list B) ≝ 111 113 match l with 112  nil => OK nil 113  hd :: tl => do hd' < f hd; do tl' < mmap f tl; OK (hd' :: tl') 114 end. 115 116 Remark mmap_inversion: 117 forall (A B: Type) (f: A > res B) (l: list A) (l': list B), 118 mmap f l = OK l' > 114 [ nil ⇒ OK ? [] 115  cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl') 116 ]. 117 118 (* 119 lemma mmap_inversion: 120 ∀A, B: Type[0]. ∀f: A > res B. ∀l: list A. ∀l': list B. 121 mmap A B f l = OK ? l' → 119 122 list_forall2 (fun x y => f x = OK y) l l'. 120 123 Proof.
Note: See TracChangeset
for help on using the changeset viewer.