# 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](http://learnyouanagda.liamoc.net/)
- [Logic Proofs with Coq, Agda, and Idris](https://queertypes.com/posts/48-logic-proofs-with-agda-coq-idris.html)
- [An Introduction to Dependent Types and Agda](http://www2.tcs.ifi.lmu.de/~abel/lehre/SS09/Fun/DepTypes.pdf)

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?

<hr/>

Have fun!