News
Assignment 3 errata
Written on 29.10.2026 10:49 by Chiara Piombi
As some of you have pointed out, the description of Exercise 3 doesn't match the file provided; it has an unnamed example instead of a theorem called Foo2, and is missing the #check for the CommSemiring instance.
I have updated the file Ex3.lean on the exercise repository; you can submit your assignment using either version since this doesn't affect the overall objective of the exercise.