Perhaps one should extend http://us2.metamath.org:88/mpeuni/conventions.html properly.
Wolf [email protected] schrieb am Montag, 19. April 2021 um 00:52:06 UTC+2: > 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/be4c21fa-12a6-4083-9fa9-8e016480cdc5n%40googlegroups.com.
