> Second, by convention we often have really long proofs instead of > splitting them up into more lemmas and sub lemmas. Splitting them up into > logical chunks turn off and really help. I think in at least some cases > there are smaller theorems that are both reusable and crying to be made > separate.
I would love to use lemmas to avoid repeating chunks of proof steps, that are only small variations of each other. Even in the early parts of Metamath there are dozens of examples, where such repetitions litter up the overall idea of the proof. Wolf -- 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/71519697-7321-48e1-ae31-a250b8d4c9ab%40googlegroups.com.
