Changeset 2178


Ignore:
Timestamp:
Jul 12, 2012, 2:56:50 PM (5 years ago)
Author:
campbell
Message:

Shift some notation into utilities.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2176 r2178  
    502502| #f1 #f2 #H12 #s * #f3 * #H23 #X @(fn_con_trans … H12 H23)
    503503] qed.
    504 
    505 notation > "vbox('let' ❬ ident v , ident p ❭ ≝ e 'in' break e')" with precedence 10
    506   for @{ match ${e} with [ mk_DPair ${ident v} ${ident p} ⇒ ${e'} ] }.
    507504
    508505axiom BadCminorProgram : String.
     
    837834] qed.
    838835
    839 notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
    840  with precedence 10
    841 for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
    842         λ${ident E}.$s ] (refl ? $t) }.
    843 
    844836definition c2ra_function (*: internal_function → internal_function*) ≝
    845837λf.
  • src/utilities/extralib.ma

    r2101 r2178  
    191191      match ${fresh p2} with [mk_Prod ${ident x} ${ident y} ⇒ $P]])}.
    192192
     193
     194notation > "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
     197notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
     198 with precedence 10
     199for @{ 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.