Changeset 2178 for src/Cminor/toRTLabs.ma
 Timestamp:
 Jul 12, 2012, 2:56:50 PM (8 years ago)
 File:

 1 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.
Note: See TracChangeset
for help on using the changeset viewer.