Published April 12, 2023
| Version 2023-04-12
Lesson
Open
Agda examples
Creators
Description
Some examples of the usage of Agda as proof assistant. Mirror of https://gitlab.com/DPDmancul/agda-examples
Abstract (English)
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
Files
DPDmancul/agda-examples-2023-04-12.zip
Files
(27.3 kB)
| Name | Size | Download all |
|---|---|---|
|
md5:ada7291640bfffa6b82eee08a60abb0b
|
27.3 kB | Preview Download |
Additional details
Related works
- Is published in
- Lesson: https://dpdmancul.gitlab.io/agda-examples (URL)
- Is supplement to
- Computational notebook: https://gitlab.com/DPDmancul/agda-examples (URL)