We can use this PR to work on extending and improving the typechecker tests and fixing any bugs that come up along the way. Specifically, we need to:
[ ] extend the positive typechecker tests to the rest of the standard library (or a reasonable subset of it if this creates too much of a burden on CI)
[ ] implement negative typechecker tests, see this discussion
[ ] (nice-to-have) expand reduction "unit tests" in Tests/Typechecker/Reduction.lean, in particular for the now-untested quotient implementation
We can use this PR to work on extending and improving the typechecker tests and fixing any bugs that come up along the way. Specifically, we need to:
Tests/Typechecker/Reduction.lean, in particular for the now-untested quotient implementation