> > So we encourage (but do not require) that people minimize their proofs > when it is not too much trouble to do so. >
Perhaps it is a bit off-topic for this thread, but I think it's worth suggesting anyway. Maybe there should be a "tutorial" page for contributing to set.mm which will explain all the steps required and some tips/suggestions (like minimizing your proof before contributing it to set.mm)? I imagine a set-by-step explanation, showing how to transfer the statement and the proof of your theorem into set.mm, how to comment it correctly, how to minimize the proof, wrap/unwrap and so on. It seems to me that set.mm accumulated a baggage of rules and conventions (some of which are, of course, covered in the "Conventions and Style" page), so having a definite first guide will make contributing more "user-friendly" and will encourage correct behavior, like minimizing theorems or writing detailed comments. -- 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/ecc1bd71-4383-4cb2-8c2c-543f55965562%40googlegroups.com.
