Learn the Agda basics in three 2-hour sessions.
This Agda tutorial was constructed by Jesper Cockx and later modified and maintained by Andreas Nuyts as part of a CS master course titled "Formal Systems and their Applications" at KU Leuven, Belgium. We decided to make it public after receiving comments that there aren't so many quick Agda tutorials out there. It is currently no longer in use at KU Leuven and therefore no longer maintained, but pull requests are welcome.
All agda code should currently be tuned for Agda 2.6.1 and the Agda standard library v1.3 (versions available via Ubuntu jammy package manager).
It is assumed you use emacs with agda-mode as your IDE. Users may wish to put the .emacs file in their homefolder.