Code samples and exercise solutions for Programming Language Foundations in Agda, an online book by Philip Wadler and Wen Kokke. I'm working through it for the SF Types, Theorems, and Programming Languages meetup.
To verify the code yourself, make sure that you've
- installed Agda and its Emacs mode, and
- added the standard library to your
librariesfile.
Then open up any of the .agda files in Emacs and type C-c C-l to typecheck it.