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

Last change on this file since 231 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
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.