equal
deleted
inserted
replaced
1 chapter Cube |
1 chapter Cube |
2 |
2 |
3 session Cube = Pure + |
3 session Cube = Pure + |
4 description \<open> |
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 Barendregt's Lambda-Cube. |
8 Barendregt's Lambda-Cube. |
9 |
9 |
10 NB: the formalization is not completely sound! It does not enforce |
10 NB: the formalization is not completely sound! It does not enforce |
11 distinctness of variable names in contexts! |
11 distinctness of variable names in contexts! |
12 |
12 |
13 For more information about the Lambda-Cube, see H. Barendregt, Introduction |
13 For more information about the Lambda-Cube, see H. Barendregt, Introduction |
14 to Generalised Type Systems, J. Functional Programming. |
14 to Generalised Type Systems, J. Functional Programming. |
15 \<close> |
15 " |
16 theories Example |
16 theories Example |