Dependent Types Assignment 2

In this assignment, you'll practice working with natural numbers and pairs in Pie. The Pie exercises cover chapters 3. You'll also being implementing an evaluator for untyped lambda calculus with integers and addition.

The Pie assignment should be completed by writing a definition for each claim, and then uncommenting the tests so that they all pass. Passing the tests is necessary, but not sufficient, for completing the exercise - you should also follow the instructions in the file.

1. Start from this file, which contains the Pie exercises
2. I provide a skeleton of the evaluator in Haskell and Racket. You may choose any language at all to implement your evaluator, but these files may provide a starting point.
3. Submit your 2.pie and your evaluator implementation, as a .tar.gz archive with all files on Gradescope. Include a README.md file that tells me how to compile and/or run your evaluator.

Gradescope Submission link https://www.gradescope.ca/courses/11611/assignments/55223

Parts of this assignment are written by David Christiansen and used with permission.