1. Terms and Proofs (21/1/2025).
  2. Recursion (30/1/2025).
  3. Inductive Types; Typeclasses (25/2/2025).

Inductive Types; Typeclasses

due by Tuesday, Feb 25, 2025

The assignment is in the course repository file TreeMem.lean. The easiest way to work on the assignment is to open the link in Lean 4 Web Editor. You can edit the file, copy its contents and submit.

Alternatively, you can fork the repository and work on the assignment in your local Lean 4 installation.

Submission

To submit, please send a direct message to me on the course Zulip server, with your solution enclosed in a code block, with the language left blank (Lean 4 is the default language).