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

Last change on this file since 235 was 228, checked in by mulligan, 10 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
RevLine 
[228]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.