equal
deleted
inserted
replaced
15 |
15 |
16 Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, |
16 Simon Thompson, Type Theory and Functional Programming (Addison-Wesley, |
17 1991) |
17 1991) |
18 *} |
18 *} |
19 options [document = false] |
19 options [document = false] |
20 theories Main |
20 theories |
|
21 Main |
21 |
22 |
22 session "CTT-ex" in ex = CTT + |
23 (* Examples for Constructive Type Theory *) |
23 description {* |
24 "ex/Typechecking" |
24 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
25 "ex/Elimination" |
25 Copyright 1991 University of Cambridge |
26 "ex/Equality" |
26 |
27 "ex/Synthesis" |
27 Examples for Constructive Type Theory. |
|
28 *} |
|
29 options [document = false] |
|
30 theories Typechecking Elimination Equality Synthesis |
|