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

Last change on this file since 277 was 268, checked in by sacerdot, 10 years ago
  • notation moved to proper places
  • new function split on Vectors
File size: 240 bytes
RevLine 
[246]1include "Universes.ma".
[228]2
3nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
[268]4{ first: A;
[228]5  second: B
[236]6}.
7
[268]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.