I think such a page would fit best as an additional HTML page on the metamath web site, which could be developed on github next to the other web pages. (I don't have any particular suggestions for what to put on the page at the moment but I'd be happy to review or extend it if someone wants to take a shot at it.)
Mario On Sun, Apr 18, 2021 at 9:48 AM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > Recently, there was (again) a discussion how to find theorems whose proofs > can be minimized by a new theorem, and how to change variables of a theorem > (and all proofs depending on this theorem). Norm and Benoît had useful > advices how to do it. I wonder if this should be documented at a central > place. Or is there already something avaiblable? > I think everybody adding new theorems to set.mm and proving them (or > shortening already existing proofs) has a lot of experience which can be > useful for others. > > Therefore, I would propose to create a "page" where How-Tos and best > practices for writing theorems and proofs for set.mm can be documented. I > do not know if the Wiki on Github would be the best place, or should it be > a *.raw.html page? > > A starting point for such a page could be the two "tasks" mentioned > above... > > Best regards, > Alexander > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/2870738f-a2af-40b2-a31b-b9aa4f8cd000n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/2870738f-a2af-40b2-a31b-b9aa4f8cd000n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStb0RPDOCBqSxii8FNywzbFz5p1e34Rprx__MBna3R9kQ%40mail.gmail.com.
