equal
deleted
inserted
replaced
3 session Cube = Pure + |
3 session Cube = Pure + |
4 description {* |
4 description {* |
5 Author: Tobias Nipkow |
5 Author: Tobias Nipkow |
6 Copyright 1992 University of Cambridge |
6 Copyright 1992 University of Cambridge |
7 |
7 |
8 The Lambda-Cube a la Barendregt. |
8 Barendregt's Lambda-Cube. |
|
9 |
|
10 NB: the formalization is not completely sound! It does not enforce |
|
11 distinctness of variable names in contexts! |
|
12 |
|
13 For more information about the Lambda-Cube, see H. Barendregt, Introduction |
|
14 to Generalised Type Systems, J. Functional Programming. |
9 *} |
15 *} |
10 options [document = false] |
16 options [document = false] |
11 theories Example |
17 theories Example |
12 |
18 |