Get started with the textbook Programming Language Foundations in Agda (PLFA).
It is recommended that you download the source:
git clone https://github.com/plfa/plfa.github.io.gitThe files corresponding to the early sections of the book are in the sub-directory
src/plfa/part1
,
see the “Source” links at the top of the web pages corresponding
to each section.
Do at least all “recommended” exercises.
Accumulate any questions you have and bring the resulting question list to class on Friday.
(The PLFA source files are litereate Agda files using MarkDown for
the documentation parts; this is one of the acceptable formats for
this course. After loading such a *.lagda.md
file in Emacs, you
may need to manually start M-x agda2-mode
to activate the special
Emacs mode for Agda, which will also give you an “Agda” menu in
the Emacs menubar.)