Changeset 2439 for src/common/Errors.ma


Ignore:
Timestamp:
Nov 7, 2012, 4:42:02 PM (7 years ago)
Author:
campbell
Message:

Get a proper reverse mapping of function blocks to identifiers by getting
rid of shadowing.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1954 r2439  
    253253notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    254254
     255lemma 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
    255264definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
    256265  match f return λx. f = x → ? with
Note: See TracChangeset for help on using the changeset viewer.