Changeset 189 for C-semantics/Errors.ma


Ignore:
Timestamp:
Oct 18, 2010, 11:36:07 AM (9 years ago)
Author:
campbell
Message:

Rework monad notation so that it is displayed well in proof mode.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Errors.ma

    r4 r189  
    6060
    6161(* Not sure what level to use *)
    62 notation "ident v ← e;: e'" right associative with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
    63 interpretation "error monad bind" 'bind e f = (bind ? ? e f).
    64 notation "〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     62notation > "vbox('do' ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
     63notation > "vbox('do' ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
     64notation < "vbox('do' \nbsp ident v ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
     65notation < "vbox('do' \nbsp ident v : ty ← e; break e')" with precedence 40 for @{'bind ${e} (λ${ident v} : ${ty}.${e'})}.
     66interpretation "error monad bind" 'bind e f = (bind ?? e f).
     67notation > "vbox('do' 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     68notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     69notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     70notation < "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'})}.
    6571interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f).
    6672(*interpretation "error monad ret" 'ret e = (ret ? e).
Note: See TracChangeset for help on using the changeset viewer.