Kevin Buzzard (Jul 04 2020 at 10:31):
I wrote mathlib's
docs/extras/simp.md when I knew barely anything about
simp; it was just some personal notes for myself which somehow ended up in mathlib. Now I understand
simp much better and feel like the docs do a very poor job of explaining the "point" of
simp -- for example they do not even mention
simp normal form (something I probably didn't understand when I wrote the md file). I just went to edit this file but I now find that it's moved to https://leanprover-community.github.io/extras/simp.html . How do I edit it now?
Markus Himmel (Jul 04 2020 at 10:34):
Patrick Massot (Jul 04 2020 at 10:36):
Note for next time : you can find the answer at the very bottom of the page.
Last updated: May 13 2021 at 19:20 UTC