Changeset 268 for Deliverables/D4.1/Matita/Cartesian.ma
 Timestamp:
 Nov 23, 2010, 5:44:42 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Cartesian.ma
r246 r268 2 2 3 3 nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝ 4 { 5 first: A; 4 { first: A; 6 5 second: B 7 6 }. 8 7 9 notation "(l,r)" 10 non associative with precedence 90 11 for @{ 'cartesian $l $r }. 12 13 interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r). 8 interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r). 9 interpretation "Cartesian" 'product A B = (Cartesian A B).
Note: See TracChangeset
for help on using the changeset viewer.