This is a small library of logic, equational reasoning, and natural numbers written in Agda. I am interested in learning about "proofs-as-programs" and how this is implemented in a system like Agda.
These files show how logic, both propositional and predicate, can be encoded in Agda.
I wrote these while studying the following excellent resources:
- Programming Language Foundations in Agda, Wadler.
- Lectures on Agda, Selinger.