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

Last change on this file since 289 was 281, checked in by mulligan, 9 years ago

Resolved conflicts.

File size: 392 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 ] }.
Note: See TracBrowser for help on using the repository browser.