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

Last change on this file since 279 was 279, checked in by sacerdot, 10 years ago

Notation moved to Cartesian.

File size: 449 bytes
Line 
1include "Universes.ma".
2
3nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝
4{ first: A;
5  second: B
6}.
7
8interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
9interpretation "Cartesian" 'product A B = (Cartesian A B).
10
11notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
12 with precedence 10
13for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
14
15(*ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).*)
16
Note: See TracBrowser for help on using the repository browser.