Safe Proof Checking in Type Theory with Y: Examples
In the article
Safe Proof Checking in Type Theory with Y,
to appear in CSL'99, we give two examples.
This page gives the input to Coq for concrete versions of these examples.
We used the following version of Coq: Coq V6.2.4 (January 1999).
- Example 1: search for a number n such that Q n holds.
- Example 2: prove a property for 0 upto n.