Coq Quote

I once asked a fellow summer school-participant if he used the Coq theorem prover. He replied that his professor discouraged him to do so since he thought it was completely incomprehensible due to all the types.

This conversation came to my mind when I read paragraph 14.1.2.3 in the Coq’Art:

An inductive definition actually contains several terms that are types. One of these terms is the type of the type being defined the others are the type of the constructors. Each of these type terms also has a type, and the inductive definition is only well-formed if the type of all these type expressions is the same up to convertibility.