- Rocq Prover 88.5%
- HTML 8.5%
- Gnuplot 2.6%
- Shell 0.3%
|
|
||
|---|---|---|
| docs | ||
| exercises | ||
| fig | ||
| md | ||
| theories | ||
| .gitignore | ||
| .nojekyll | ||
| _CoqProject | ||
| dune | ||
| dune-project | ||
| index.html | ||
| LICENSE | ||
| README.md | ||
| TODO.md | ||
| tutorial.mv | ||
| waterproof-reference-sheet.md | ||
Analysis lectures material
This repository contains course material for the Analysis course at the University of Groningen.
The lectures material can be accessed at mseri.me/analysis_rug. This contains both the syllabus, including tutorial exercises, and navigable slides for the lectures.
The theories folder contains the content of the lectures, separated in thematic sections, formalized in Waterproof (WIP).
The exercises folder contains the barebone homework exercises in Waterproof format, ready to be formalized.
Waterproof
Waterproof is educational software designed to help students with learning the skill of proving mathematical statements. It uses a natural syntax that makes the exercise very close to what one would write on paper. The software checks the correctness of the proofs and provides feedback to the user. See here for more information.
Part of the material, for instance the tutorial, is based on the one available from the waterproof-exercise-sheets and introduction-to-proofs repositories.
Tutorial
This repository also contains an edited version of the Waterproof tutorial, tutorial.mv, which explains how to use Waterproof's custom proof language with very simple examples.
Quickstart
Quickstart (in browser)
You can try out these exercises in Github codespaces, which is a service that offers a free number of hours per month. 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 Github codespace environment after using it.
Quickstart (local)
- Download the exercises and unzip them in a new folder.
- Go to https://vscode.dev?enable-coi using Google Chrome or Chromium.
- Go to extensions (Ctrl+Shift+x or Cmd+Shift+x), search for Waterproof and install it (choose to "trust" the extension).
- Go to files (Ctrl+Shift+e or Cmd+Shift+x), click "Open folder" and choose the folder from step 1 (choose to "trust" the folder).
- If the browser asks for permission to view or edit files in that location, allow this.
- Open the relevant
.mvfile, for instancetutorial.mv. - If everything installed correctly, you should see a "Goal" window on the right, which shows what is left to prove when you click in the text of proofs.