1chapter Cube 2 3session Cube = Pure + 4 description " 5 Author: Tobias Nipkow 6 Copyright 1992 University of Cambridge 7 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. 15 " 16 theories Example 17