CTT: Constructive Type Theory

This directory contains the ML sources of the Isabelle system for Constructive Type Theory (extensional equality, no universes).

The ex subdirectory contains some examples.

Useful references on Constructive Type Theory: