source:
Deliverables/D4.1/Matita/Cartesian.ma
@
327
| Last change on this file since 327 was 281, checked in by , 10 years ago | |
|---|---|
| File size: 392 bytes | |
| Line | |
|---|---|
| 1 | include "Universes.ma". |
| 2 | |
| 3 | nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝ |
| 4 | { first: A; |
| 5 | second: B |
| 6 | }. |
| 7 | |
| 8 | interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r). |
| 9 | interpretation "Cartesian" 'product A B = (Cartesian A B). |
| 10 | |
| 11 | notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" |
| 12 | with precedence 10 |
| 13 | for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }. |
Note: See TracBrowser
for help on using the repository browser.
