Homepage update and exercises
Jan Malakhovski
Update at the home page (http://oxij.org/activity/ttfv/). Now it has
"We are here!" marker and striked out topics, most of which (without
an explicit link on the right hand side) could be found in
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385
Defining lambda interpreter in lambda should be obvious (write it in
Haskell and use "Untyped Haskell" translation).
You could do this as an exercise.
The attachment has some relatively simple exercises for those who have
already started playing with Agda.
I strongly recommend to check out this page
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations
before diving in.
These combinations particularly:
C-c C-, Goal type and context
C-u C-c C-, Goal type and context (without normalising)
C-c C-. Goal type and inferred type
C-u C-c C-. Goal type and inferred type (without normalising)
Do not use Auto, use paper.
Also, pretty useful pattern:
(\lambda x \to _) (?)
if you define _$_ f x = f x then you could simply write:
_ $ term
It will force Agda to generate an unsolved constraint that will show
the difference between the goal and the things your "term" actually
proves.
Extremely useful with Give and Refine (you don't have to stop
everything with C-c-x-d if something in the term is not quite right
yet).
Have fun,
Jan