| changeset 283 | 76caebd18756 |
| parent 23 | 1cd377c2f7c6 |
| child 1149 | 5750eba8820d |
| 282:731b27c90d2f | 283:76caebd18756 |
|---|---|
6 Constructive Type Theory |
6 Constructive Type Theory |
7 *) |
7 *) |
8 |
8 |
9 CTT = Pure + |
9 CTT = Pure + |
10 |
10 |
11 types i,t,o 0 |
11 types |
12 |
12 i |
13 arities i,t,o :: logic |
13 t |
14 o |
|
15 |
|
16 arities |
|
17 i,t,o :: logic |
|
14 |
18 |
15 consts |
19 consts |
16 (*Types*) |
20 (*Types*) |
17 F,T :: "t" (*F is empty, T contains one element*) |
21 F,T :: "t" (*F is empty, T contains one element*) |
18 contr :: "i=>i" |
22 contr :: "i=>i" |