Changeset 2439 for src/common/Errors.ma
 Timestamp:
 Nov 7, 2012, 4:42:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r1954 r2439 253 253 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 254 254 255 lemma bind_as_inversion: 256 ∀A,B: Type[0]. ∀f: res A. ∀g: ∀a:A. f = OK A a → res B. ∀y: B. 257 (do x as E ← f; g x E = return y) → 258 ∃x. ∃E:f = return x. g x E = return y. 259 #A #B #f cases f normalize 260 [ #a #g #y #e %{a} /2/ 261  #m #g #y #H destruct (H) 262 ] qed. 263 255 264 definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. 256 265 match f return λx. f = x → ? with
Note: See TracChangeset
for help on using the changeset viewer.