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

Terms and Proofs

due by Tuesday, Jan 21, 2025

The assignment is in the course repository file TermsAndProofs.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).