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

Last change on this file since 228 was 228, checked in by mulligan, 9 years ago

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 110 bytes
Line 
1include "logic/pts.ma".
2
3nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
4{
5  first: A;
6  second: B
7}.
Note: See TracBrowser for help on using the repository browser.