Agda is a dependently typed functional programming language as well as a proof assistant.
Examples
- Literate Agda Semantics - Syntax
- binary representation of Natural: Agda Cat: The “bits” Challenge - gelisam
Agda is a dependently typed functional programming language as well as a proof assistant.
This work is licensed under a Creative Commons Attribution 4.0 International License