| author | wenzelm |
| Tue, 17 Dec 2019 22:18:37 +0100 | |
| changeset 71302 | 0e3a3e3cf482 |
| parent 69319 | baccaf89ca0d |
| child 75992 | 1f6d79b62222 |
| permissions | -rw-r--r-- |
|
51397
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
1 |
chapter Cube |
|
03b586ee5930
support for 'chapter' specifications within session ROOT;
wenzelm
parents:
48738
diff
changeset
|
2 |
|
|
48738
f8c1a5b9488f
simplified session specifications: names are taken verbatim and current directory is default;
wenzelm
parents:
48483
diff
changeset
|
3 |
session Cube = Pure + |
| 69319 | 4 |
description " |
| 48475 | 5 |
Author: Tobias Nipkow |
6 |
Copyright 1992 University of Cambridge |
|
7 |
||
|
51403
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
8 |
Barendregt's Lambda-Cube. |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
9 |
|
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
10 |
NB: the formalization is not completely sound! It does not enforce |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
11 |
distinctness of variable names in contexts! |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
12 |
|
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
13 |
For more information about the Lambda-Cube, see H. Barendregt, Introduction |
|
2ff3a5589b05
refurbished some old README.html files as session descriptions, which show up in chapter index;
wenzelm
parents:
51397
diff
changeset
|
14 |
to Generalised Type Systems, J. Functional Programming. |
| 69319 | 15 |
" |
| 48475 | 16 |
theories Example |