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 | |
| Rev | Line | |
|---|---|---|
| [246] | 1 | include "Universes.ma". |
| [228] | 2 | |
| 3 | nrecord Cartesian (A: Type[0]) (B: Type[0]): Type[0] ≝ | |
| [268] | 4 | { first: A; |
| [228] | 5 | second: B |
| [236] | 6 | }. |
| 7 | ||
| [268] | 8 | interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r). |
| 9 | interpretation "Cartesian" 'product A B = (Cartesian A B). | |
| [279] | 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.
