Agda is a proof assistant based on Martin-Löf type theory, which syntax is highly inspired by Haskell, a functional language. Proof assistants help writing proofs and check them are correct.
Here are reported some examples of the usage of Agda as proof assistant, used as help material during an introductive lecture to proof assistants.
You can click on the symbols in the code to see their definition: this is very useful in particular for standard library items which definition is not reported in the examples.
View video of the lecture (in italian).
View the interactive HTML version.
See table of contents.
- Clone the repo https://gitlab.com/DPDmancul/agda-examples.git
- Optionally run
nix-shellto get all the required dependencies into the environment - Just run
maketo generate the HTML book.
To edit the files you can use your favourite editor (Agdapad, (Neo)Vim, ...) or, if you are using NixOs, the agda-preconfigured evil emacs-nox shipped with this code: make edit.
© 2022 Davide Peressoni
This work is licensed under both the Apache 2.0 License and the Creative Commons Attribution-ShareAlike 4.0 International License.
Attribution -- You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
ShareAlike -- If you remix, transform, or build upon the material, you must distribute your contributions under the same license as the original.
The source files can be found at https://gitlab.com/DPDmancul/agda-examples.