equal
deleted
inserted
replaced
2 |
2 |
3 session CTT = Pure + |
3 session CTT = Pure + |
4 description {* |
4 description {* |
5 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
5 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6 Copyright 1991 University of Cambridge |
6 Copyright 1991 University of Cambridge |
|
7 |
|
8 This is a version of Constructive Type Theory (extensional equality, |
|
9 no universes). |
|
10 |
|
11 Useful references on Constructive Type Theory: |
|
12 |
|
13 B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf's |
|
14 Type Theory (Oxford University Press, 1990) |
|
15 |
|
16 Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, |
|
17 1991) |
7 *} |
18 *} |
8 options [document = false] |
19 options [document = false] |
9 theories Main |
20 theories Main |
10 |
21 |
11 session "CTT-ex" in ex = CTT + |
22 session "CTT-ex" in ex = CTT + |