source: Deliverables/D4.1/Matita/Cartesian.ma @ 268

Last change on this file since 268 was 268, checked in by sacerdot, 10 years ago
  • notation moved to proper places
  • new function split on Vectors
File size: 240 bytes
Line 
1include "Universes.ma".
2
3nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
4{ first: A;
5  second: B
6}.
7
8interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
9interpretation "Cartesian" 'product A B = (Cartesian A B).
Note: See TracBrowser for help on using the repository browser.