Changeset 1626 for src/common


Ignore:
Timestamp:
Dec 19, 2011, 2:48:33 PM (8 years ago)
Author:
campbell
Message:

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1609 r1626  
    303303notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    304304
     305definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
     306  match f return λx. f = x → ? with
     307  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
     308  | Error msg ⇒ λ_. Error ? msg
     309  ] (refl ? f).
     310
     311notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 40 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.
     312
    305313definition res_to_opt : ∀A:Type[0]. res A → option A ≝
    306314 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].
Note: See TracChangeset for help on using the changeset viewer.