This directory contains the homework.

For each weak i, with i = 1, 2, 3 etc.
you have files lecture0i.v and possibly lecture0ia.v, lecture0ib.v...
You should consider the files in this order 0i, 0ia, 0ib, etc.

Run each file in your favorite environment, e.g. proofgeneral or coqIDE,
and complete the exercises.
Then return a file which should be syntactically correct.
That is, entering it in coqtop (or running coqc on it) should succeed.
If you cannot finish some exercises, use admit (for direct definitions)
and Admitted (for interactive definitions/proofs).
You can add material in comments 
(* 
  Your ideas
*)

You are completely successful if no admit and Admitted is left.


Additionnally, this directory contains library files such
as tests_nat.v.
Such files can be compiled in the following way:
     - CoqIDE
   
       1. Open tests_nat.v.
       2. In the "Compile" menu, click on "Compile Buffer".
   
     - Command line
   
       1. Run: coqc tests_nat.v

Then you get tests_nat.vo (This is like making a .o file from a .c file.),
which can in turn be used in another coq file as follows:
Require Import tests_nat.