| author | paulson <lp15@cam.ac.uk> | 
| Tue, 02 Nov 2021 17:01:47 +0000 | |
| changeset 74668 | 2d9d02beaf96 | 
| 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  |