Changeset 2453 for src/utilities/monad.ma
 Timestamp:
 Nov 12, 2012, 4:30:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/monad.ma
r2179 r2453 28 28 }. 29 29 30 notation "m »= f" with precedence 4931 for @{'m_bind $m $f }. 30 (* notation "m »= f" with precedence 49 31 for @{'m_bind $m $f }. *) 32 32 33 33 notation > "!_ e; e'" … … 37 37 notation > "! ident v : ty ← e; e'" 38 38 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 39 notation < "vbox(! \nbsp ident v ← e ; break e')"40 with precedence 48 for @{'m_bind ${e} (λ${ident v}.${e'})}.41 39 notation > "! ident v ← e : ty ; e'" 42 40 with precedence 48 for @{'m_bind (${e} : ${ty}) (λ${ident v}.${e'})}. 43 notation < "vbox(! \nbsp ident v : ty \nbsp ← \nbsp e ;break e')"41 notation < "vbox(! \nbsp hvbox( ident v : ty \nbsp break ← \nbsp e ;) break e')" 44 42 with precedence 48 for @{'m_bind ${e} (λ${ident v} : ${ty}. ${e'})}. 45 43 notation > "! ident v : ty ← e : ty' ; e'" … … 51 49 notation > "! 〈ident v1 : ty1, ident v2 : ty2〉 ← e ; e'" 52 50 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. 53 notation < "vbox(! \nbsp 〈ident v1, ident v2〉 ← e ; break e')" 54 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1}. λ${ident v2}. ${e'})}. 55 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 \nbsp ← \nbsp e ; break e')" 51 notation < "vbox(! \nbsp hvbox( 〈ident v1 : ty1, break ident v2 : ty2〉 \nbsp break ← \nbsp e ; ) break e')" 56 52 with precedence 48 for @{'m_bind2 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. ${e'})}. 57 53 notation > "! 〈ident v1, ident v2, ident v3〉 ← e ; e'" … … 61 57 notation > "! 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 ← e ; e'" 62 58 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. 63 notation < "vbox(! \nbsp 〈ident v1, ident v2, ident v3〉 \nbsp ← \nbsp e ; break e')" 64 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1}. λ${ident v2}. λ${ident v3}. ${e'})}. 65 notation < "vbox(! \nbsp 〈ident v1 : ty1, ident v2 : ty2, ident v3 : ty3〉 \nbsp ← e \nbsp ; break e')" 59 notation < "vbox(! \nbsp hvbox( 〈ident v1 : ty1, break ident v2 : ty2, break ident v3 : ty3〉 \nbsp break ← e \nbsp ; ) break e')" 66 60 with precedence 48 for @{'m_bind3 ${e} (λ${ident v1} : ${ty1}. λ${ident v2} : ${ty2}. λ${ident v3} : ${ty3}. ${e'})}. 67 61 … … 71 65 @{'m_bind ${e} (λ${fresh p_sig}. 72 66 match ${fresh p_sig} with [mk_Sig ${ident v1} ${ident v2} ⇒ ${e'}])}. 73 notation < "vbox(! \nbsp «ident v1, ident v2» \nbsp ← \nbsp e ;break e')"67 notation < "vbox(! \nbsp hvbox( «ident v1, break ident v2» \nbsp break ← \nbsp e ; ) break e')" 74 68 with precedence 48 for 75 69 @{'m_bind ${e} (λ${fresh p_sig}. … … 79 73 with precedence 48 for 80 74 @{'m_sigbind2 ${e} (λ${ident v1},${ident v2},${ident H}. ${e'})}. 81 notation < "vbox(! \nbsp «ident v1, ident v2, ident H» \nbsp ← \nbsp e ;e')"75 notation < "vbox(! \nbsp hvbox( «ident v1, break ident v2, break ident H» \nbsp break ← \nbsp e ; ) e')" 82 76 with precedence 48 for 83 77 @{'m_sigbind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}. … … 144 138 ; sm_eq_sym : ∀X.symmetric ? (sm_eq X) 145 139 ; sm_return_proper : ∀X,x.sm_eq X (return x) (return x) 146 ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y ( x »= f) (y »=g)140 ; sm_bind_proper : ∀X,Y,x,y,f,g.sm_eq X x y → (∀x.sm_eq Y (f x) (g x)) → sm_eq Y (m_bind … x f) (m_bind … y g) 147 141 ; sm_return_bind : ∀X,Y.∀x : X.∀f : X → smax_def Y. 148 142 sm_eq Y (! y ← return x ; f y) (f x)
Note: See TracChangeset
for help on using the changeset viewer.