Changeset 2179


Ignore:
Timestamp:
Jul 12, 2012, 2:56:51 PM (5 years ago)
Author:
campbell
Message:

Dependent pair monad binding notation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/monad.ma

    r1976 r2179  
    115115  @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}.
    116116
     117notation > "'do' ❬ident v1, ident v2❭ ← e ; e'"
     118  with precedence 48 for
     119  @{'m_bind ${e} (λ${fresh p_sig}.
     120    match ${fresh p_sig} with [mk_DPair ${ident v1} ${ident v2} ⇒ ${e'}])}.
     121
    117122notation > "'return' t" with precedence 49 for @{'m_return $t}.
    118123notation < "'return' \nbsp t" with precedence 49 for @{'m_return $t}.
Note: See TracChangeset for help on using the changeset viewer.