Type-checking PTS (sources)

Graph of dependencies generated by Dependtohtml
Since the development is parametric, the parameters are defined in the main file, which glues together all the others, using Load. Theory of PTS with abstract subtyping: First example of subtyping: when the subtyping relation is the reflexive-symmetric-transitive closure of a reduction rule: Second example: the subtyping relation is cumulativity, parameterized by the inclusion between sorts and a reduction rule: Examples of reduction rules: beta and delta
Examples of sort inclusion:
Library files:
Coq files compiled on: Dec 23 1998 15:55:19

The Coq Proof Assistant, version V6.2.3 - Type not extracted (December 1998)
compiled on Dec 18 1998 20:29:23