To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.


Exercise 1:

  • Let's define the subtype of odd and even natural numbers
  • Intrument Coq to recognize odd/even number built out of product and successor
  • Inherit on odd_nat the eqType structure