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

Last change on this file since 257 was 246, checked in by mulligan, 9 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.