This repository contains what I wrote while working through "Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version)" by David Thrane Christiansen. A good chunk of the work was done back in January when I was just learning Idris.

It looks like I organized things:

• src/Main2.idr Material for Section 1, with a parser appended.
• src/Main3.idr Includes the changes in section 3
• src/Main4.idr Includes the changes in section 4
• src/Main5.idr Includes the changes from section 5
• src/Tartlet.idr Includes section 6 and the beginnings of a REPL