Elements of Agda programming
Code examples / exercises
First session (a bit of Agda)
Second session (equational reasoning
with addition and multiplication)
Third session (playing with
relation, unicity and some simplification techniques)
Fourth session (playing with
order, list and sorting)