Changeset 1598 for src/utilities
 Timestamp:
 Dec 12, 2011, 5:53:36 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/pair.ma
r1316 r1598 3 3 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 4 4 with precedence 10 5 for @{ match $t with [ pair${ident x} ${ident y} ⇒ $s ] }.5 for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }. 6 6 7 7 (* Also extracts an equality proof (useful when not using Russell). *) 8 8 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" 9 9 with precedence 10 10 for @{ match $t return λx.x = $t → ? with [ pair${ident x} ${ident y} ⇒10 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒ 11 11 λ${ident E}.$s ] (refl ? $t) }. 12 12 13 13 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)" 14 14 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} ⇒15 for @{ 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} ⇒ 17 17 λ${ident E}.$s ] ] (refl ? $t) }. 18 18
Note: See TracChangeset
for help on using the changeset viewer.