Ok, so this is very interesting, I see others think so too, as they upvote it, but could someone offer an explanation of what exactly is going on here? I would love to have a little glossary of Agda syntax and concepts to go with this post; as it is now it's completely undecipherable for me, unfortunately :(
Ok, so this is very interesting, I see others think so too, as they upvote it, but could someone offer an explanation of what exactly is going on here? I would love to have a little glossary of Agda syntax and concepts to go with this post; as it is now it's completely undecipherable for me, unfortunately :(
(these are just cribbed from the agda wikipedia page but..) check these out:
http://www.youtube.com/playlist?p=B7F836675DCE009C
http://www.cse.chalmers.se/~ulfn/papers/tphols09/tutorial.pd...