Changeset 2178 for src

Timestamp:

Jul 12, 2012, 2:56:50 PM (9 years ago)

Author:

campbell

Message:

Shift some notation into utilities.

Location:

src

Files:

• Cminor/toRTLabs.ma (modified) (2 diffs)
• utilities/extralib.ma (modified) (1 diff)

src/Cminor/toRTLabs.ma

@@ -502 +502 @@
 | #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
 ] qed.
-
-notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
-  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
 
 axiom BadCminorProgram : String.
@@ -837 +834 @@
 ] qed.
 
-notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
- with precedence 10
-for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
-        λ${ident E}.$s ] (refl ? $t) }.
-
 definition c2ra_function (*: internal_function → internal_function*) ≝
 λf.

src/utilities/extralib.ma

@@ -191 +191 @@
       match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
 
+
+notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
+  for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
+
+notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
+        λ${ident E}.$s ] (refl ? $t) }.