Changeset 764 for src/common/Errors.ma
 Timestamp:
 Apr 20, 2011, 5:38:58 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Errors.ma
r695 r764 61 61 ]. 62 62 63 definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D. 64 match f with 65 [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ] 66  Error (*msg*) => Error ? (*msg*) 67 ]. 68 63 69 (* Not sure what level to use *) 64 70 notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}. … … 72 78 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}. 73 79 interpretation "error monad Prod bind" 'bind2 e f = (bind2 ??? e f). 80 notation > "vbox('do' 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}. 81 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}. 82 notation < "vbox('do' \nbsp 〈ident v1, ident v2, ident v3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1}.λ${ident v2}.λ${ident v3}.${e'})}. 83 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e; break e')" with precedence 40 for @{'bind3 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.λ${ident v3} : ${ty3}.${e'})}. 84 interpretation "error monad triple bind" 'bind3 e f = (bind3 ???? e f). 74 85 (*interpretation "error monad ret" 'ret e = (ret ? e). 75 86 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
Note: See TracChangeset
for help on using the changeset viewer.