Dependent Types Assignment 6

In this assignment, you'll continue practicing with induction on natural numbers and the equality type. The Pie exercises cover Chapter 8 and 9.

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. Submit your 6.pie file on Gradescope.

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