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

Shift some notation into utilities.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.