Changeset 1323 for src/ASM/Util.ma

Timestamp:

Oct 7, 2011, 3:26:36 PM (8 years ago)

Author:

campbell

Message:

Reduce number of notations for destructive let on pairs to one.

File:

• src/ASM/Util.ma (modified) (2 diffs)

src/ASM/Util.ma

@@ -3 +3 @@
 include "arithmetics/nat.ma".
 
+include "utilities/pair.ma".
 include "ASM/JMCoercions.ma".
 
@@ -13 +14 @@
 notation "⊥" with precedence 90
   for @{ match ? in False with [ ] }.
-
-notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
- with precedence 10
-for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
-
-(*
-notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
- with precedence 10
-for @{
-  match $t with
-  [ pair ${ident x} y' ⇒
-    match y' with
-    [ pair ${ident y} ${ident z} ⇒ $s ]
-  ]
-}.
-*)
 
 definition ltb ≝