Changeset 279 for Deliverables/D4.1/Matita/Cartesian.ma
 Timestamp:
 Nov 24, 2010, 5:19:38 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Cartesian.ma
r268 r279 8 8 interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r). 9 9 interpretation "Cartesian" 'product A B = (Cartesian A B). 10 11 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 12 with precedence 10 13 for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }. 14 15 (*ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).*) 16
Note: See TracChangeset
for help on using the changeset viewer.