Dependent Products

All the examples of the chapter

This file contains all the coq source included in the chapter about the depend product. We advise the surfer to download it, re-run all the examples, and try to change the proofs whenever possible. Download this file

Exercises


Exercise 4.1 page 76 Some types in the calculus of constructions
Exercise 4.2 page 90 A polymorphic functional
Polymorphic minimal logic
Exercises 4.3 page 93 and 4.5 page 97 Some inference rules
Exercise 4.4 page 96 Some simple polymorphic functions

Errata