Tag Archives: quotients

Equality part 1: definitional equality.

I keep meaning to write something about equality in Lean, and on the tube home today I just managed to understand it a little bit better, so perhaps now is the time (although I won’t get to today’s revelation until … Continue reading

Posted in Learning Lean | Tagged , | 1 Comment