| changeset 58889 | 5b7a9633cfa8 |
| parent 41526 | 54b4686704af |
| child 58963 | 26bf09b95dda |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
4 |
4 |
5 Some examples taken from P. Martin-L\"of, Intuitionistic type theory |
5 Some examples taken from P. Martin-L\"of, Intuitionistic type theory |
6 (Bibliopolis, 1984). |
6 (Bibliopolis, 1984). |
7 *) |
7 *) |
8 |
8 |
9 header "Examples with elimination rules" |
9 section "Examples with elimination rules" |
10 |
10 |
11 theory Elimination |
11 theory Elimination |
12 imports CTT |
12 imports CTT |
13 begin |
13 begin |
14 |
14 |