 Timestamp:
 Apr 20, 2011, 5:38:58 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r746 r764 86 86 with precedence 10 87 87 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 88 89 (* Yeah, I probably ought to do something more general... *) 90 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)" 91 with precedence 90 for @{ 'triple $a $b $c}. 92 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z). 93 94 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" 95 with precedence 10 96 for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }. 88 97 89 98 notation "⊥" with precedence 90
Note: See TracChangeset
for help on using the changeset viewer.