A bad practice (too common unfortunately): long proofs. Often with long proofs, there is a lot of code inside them that could be refactored as useful lemmas on their own. Without this refactoring, this code is buried inside proofs and can't be used outside, so it is lost. This bad practice ultimately leads to a lot of duplicate code.
So, please refactore your proofs :mine:
Last updated: Aug 15 2022 at 02:13 UTC