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

Last change on this file since 249 was 246, checked in by mulligan, 10 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

File size: 273 bytes
Line 
1include "Universes.ma".
2
3nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
4{
5  first: A;
6  second: B
7}.
8
9notation "(l,r)"
10  non associative with precedence 90
11  for @{ 'cartesian $l $r }.
12 
13interpretation "Cartesian product" 'cartesian l r = (mk_Cartesian ? ? l r).
Note: See TracBrowser for help on using the repository browser.