Olive

Stream: new members

[Kevin Buzzard]

Curses! My design decision to cripple rw certainly sometimes causes confusion but people didn't see how confused my undergraduates were when rw randomly closed goals like x+0=x. I made a deliberate decision not to teach the concept of definitional equality and unfortunately this is the collateral damage.