Changeset 907 for src/ASM/Util.ma
 Timestamp:
 Jun 8, 2011, 6:15:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r900 r907 189 189 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z). 190 190 191 notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)" 192 with precedence 90 for @{ 'quadruple $a $b $c $d}. 193 interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)). 194 195 notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" 196 with precedence 10 197 for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }. 198 191 199 notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" 192 200 with precedence 10
Note: See TracChangeset
for help on using the changeset viewer.