I believe it's more just how to use a dependently typed language (my copy is still in the mail). Like the Little Schemer, it's written in the Socratic style. I

I believe it's more just how to use a dependently typed language (my copy is still in the mail). Like the Little Schemer, it's written in the Socratic style. I think the idea is that you can do it all in your head if you want, with a piece of paper covering up the column with the answers. If you are interested in the implementation, you can read more about it from one of the authors: http://davidchristiansen.dk/tutorials/nbe/ http://davidchristiansen.dk/tutorials/nbe/