`rw`: wrong error message
Opened this issue · 1 comments
joneugster commented
rw [lemma_wth_typo] with a non-existing lemma yields a wrong error message.
joneugster commented
I have no idea about this. If I rename our macro to anything but rewrite or rw, it shows "unknown identifier 'mul_comm'", but as soon as I name it rw that dissapears :(