## Homepage update and exercises

Showing 1-1 of 1 messages
 Homepage update and exercises Jan Malakhovski 4/21/12 9:07 AM Ladies and Gentleman,Update at the home page (http://oxij.org/activity/ttfv/). Now it has"We are here!" marker and striked out topics, most of which (withoutan explicit link on the right hand side) could be found inhttp://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7385Defining lambda interpreter in lambda should be obvious (write it inHaskell and use "Untyped Haskell" translation).You could do this as an exercise.The attachment has some relatively simple exercises for those who havealready started playing with Agda.I strongly recommend to check out this pagehttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinationsbefore diving in.These combinations particularly:C-c C-,        Goal type and contextC-u C-c C-,        Goal type and context (without normalising)C-c C-.        Goal type and inferred typeC-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: _$ termIt will force Agda to generate an unsolved constraint that will showthe difference between the goal and the things your "term" actuallyproves.Extremely useful with Give and Refine (you don't have to stopeverything with C-c-x-d if something in the term is not quite rightyet).Have fun,  Jan