The take-home midterm is now available. It is due Tuesday, October 13 at 11:59pm.
Download the exam:
Basics.v through Poly.vUnless stated otherwise, use only definitions from Basics.v through Poly.v and any lemmas proved there. Rocq proofs must be written so that Rocq would accept them. Informal proofs must describe the proof rather than mimic a Rocq script. Document all proofs: identify induction variables, proof cases, where an induction hypothesis is used, and the rewrites and lemma applications performed. This matters far more than perfect syntax.