This repository contains examples of Waterproof exercise sheets. Waterproof is an adaptation of the Coq proof assistant developed for use in mathematics education. Students type out their proofs in Waterproof and get immediate feedback on every proof step. Unlike with the default Coq proof assistant, Waterproof comes with a custom proof language that allows proofs to be written in a style similar to handwritten proofs.
These exercises are used to supplement the teaching of Analysis 1 at the TU/e. Instead of handing in their homework like usual, students can opt to hand in a completed exercise sheet. The numbering of the exercises refers to the lecture notes written by the lecturer, Jim Portegies.
There are two options to try out these Waterproof exercise sheets in your browser: through Gitpod and through Github codespaces. Both services provide a free number of hours per month.
Please note that the above link always opens up a new workspace. If you want to resume a previously opened workspace, then it is better to visit https://gitpod.io/workspaces.
To open the exercises in Github codespaces, you can click on the following link.
This link should give you the option of continuing in an earlier opened workspace, if you have opened these exercises in codespaces before.
Tip: make sure you close your Gitpod workspace or Github codespace envorinment after using it.
This repository also contains the Waterproof tutorial, tutorial.mv, which explains how to use Waterproof's custom proof language.