do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
chapter CTT
session CTT = Pure +
description {*
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
This is a version of Constructive Type Theory (extensional equality,
no universes).
Useful references on Constructive Type Theory:
B. Nordström, K. Petersson and J. M. Smith, Programming in Martin-Löf's
Type Theory (Oxford University Press, 1990)
Simon Thompson, Type Theory and Functional Programming (Addison-Wesley,
1991)
*}
options [document = false]
theories
Main
(* Examples for Constructive Type Theory *)
"ex/Typechecking"
"ex/Elimination"
"ex/Equality"
"ex/Synthesis"