Changeset 189 for C-semantics/IOMonad.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/IOMonad.ma

    r125 r189  
    3333
    3434(* If the original definitions are vague enough, do I need to do this? *)
    35 notation "! ident v ← e;: e'" right associative with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
    36 notation "! 〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     35notation > "! ident v ← e;: e'" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
     36notation > "! ident v : ty ← e;: e'" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
     37notation < "vbox(! \nbsp ident v ← e;: e')" with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
     38notation < "vbox(! \nbsp ident v : ty ← e;: e')" with precedence 40 for @{'bindIO ${e} (λ${ident v} : ${ty}.${e'})}.
     39notation > "! 〈ident v1, ident v2〉 ← e;: e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     40notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e;: e'" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
     41notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e;: e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     42notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e;: e')" with precedence 40 for @{'bindIO2 ${e} (λ${ident v1} : ${ty2}.λ${ident v2} : ${ty2}.${e'})}.
    3743interpretation "IO monad bind" 'bindIO e f = (bindIO ???? e f).
    3844interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ????? e f).
Note: See TracChangeset for help on using the changeset viewer.