Do obejrzenia razem:

* Rlogika.v

* CoqSurvivalKit.pdf

Do samodzielnego zrobienia:

* coqITP2015-ex1.v
* logikaCPDT.v
* coqITP2015-ex2.v

Zadania w plikach coqITP2015-ex1.v i coqITP2015-ex2.v pochodzą ze strony

https://coq.inria.fr/coq-itp-2015

Uwaga: tam też są rozwiązania !

Zadania z logikaCPDT.v pochodzą z książki "Certified Programming with Dependent Types"