Changeset 2178
 Timestamp:
 Jul 12, 2012, 2:56:50 PM (5 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r2176 r2178 502 502  #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23) 503 503 ] qed. 504 505 notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10506 for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.507 504 508 505 axiom BadCminorProgram : String. … … 837 834 ] qed. 838 835 839 notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"840 with precedence 10841 for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒842 λ${ident E}.$s ] (refl ? $t) }.843 844 836 definition c2ra_function (*: internal_function → internal_function*) ≝ 845 837 λf. 
src/utilities/extralib.ma
r2101 r2178 191 191 match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}. 192 192 193 194 notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10 195 for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }. 196 197 notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)" 198 with precedence 10 199 for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒ 200 λ${ident E}.$s ] (refl ? $t) }.
Note: See TracChangeset
for help on using the changeset viewer.