agda doodles
Some Agda programs that I’ve doodled with to get a feel for the language. The usual stuff, Peano arithmetic, basic proofs, et al. Nothing new, and mostly derived from various tutorials and blog posts, most notably:
- Learn You an Agda
- Logic Proofs with Coq, Agda, and Idris
- An Introduction to Dependent Types and Agda
A single proof was done by myself without help—well, except for Agda’s: the associativity of disjunction (found in Peano). It might well be that it’s complete and utter bollocks, but it seems to check out, so it’s good enough for me?
Have fun!