Changeset 1598 for src/utilities/pair.ma


Ignore:
Timestamp:
Dec 12, 2011, 5:53:36 PM (8 years ago)
Author:
mulligan
Message:

changes over the last couple of days

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/pair.ma

    r1316 r1598  
    33notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    44 with precedence 10
    5 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     5for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
    66
    77(* Also extracts an equality proof (useful when not using Russell). *)
    88notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
    99 with precedence 10
    10 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
     10for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
    1111        λ${ident E}.$s ] (refl ? $t) }.
    1212
    1313notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    1414 with precedence 10
    15 for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
    16        match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
     15for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
     16       match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
    1717        λ${ident E}.$s ] ] (refl ? $t) }.
    1818
Note: See TracChangeset for help on using the changeset viewer.