equal
deleted
inserted
replaced
1 %% $Id$ 
1 %% $Id$ 
2 \chapter{Constructive Type Theory} 
2 \chapter{Constructive Type Theory} 
3 \index{Constructive Type Theory(} 
3 \index{Constructive Type Theory(} 

4 

5 \underscoreoff %this file contains _ in rule names 
4 
6 
5 MartinL\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can 
7 MartinL\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can 
6 be viewed at many different levels. It is a formal system that embodies 
8 be viewed at many different levels. It is a formal system that embodies 
7 the principles of intuitionistic mathematics; it embodies the 
9 the principles of intuitionistic mathematics; it embodies the 
8 interpretation of propositions as types; it is a vehicle for deriving 
10 interpretation of propositions as types; it is a vehicle for deriving 