Changeset 1323 for src/ASM/Util.ma
- Timestamp:
- Oct 7, 2011, 3:26:36 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r1279 r1323 3 3 include "arithmetics/nat.ma". 4 4 5 include "utilities/pair.ma". 5 6 include "ASM/JMCoercions.ma". 6 7 … … 13 14 notation "⊥" with precedence 90 14 15 for @{ match ? in False with [ ] }. 15 16 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"17 with precedence 1018 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.19 20 (*21 notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"22 with precedence 1023 for @{24 match $t with25 [ pair ${ident x} y' ⇒26 match y' with27 [ pair ${ident y} ${ident z} ⇒ $s ]28 ]29 }.30 *)31 16 32 17 definition ltb ≝
Note: See TracChangeset
for help on using the changeset viewer.