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.
