Zulip Chat Archive

Stream: general

Topic: editing simp doc on community website

view this post on Zulip 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?

view this post on Zulip Markus Himmel (Jul 04 2020 at 10:34):

The file is at https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/extras/simp.md

view this post on Zulip 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