> > *"Rules" for introducing new definitions* > > Definitions are at the heart of achieving simplicity. While developing > set.mm, two rules of thumb that evolved in my own work were (1) there > shouldn't be two definitions that mean almost the same thing and (2) > definitions shouldn't be introduced unless there is an actual need in the > work at hand. Maybe I should add (3), don't formally define something that > doesn't help proofs and can be stated simply in English in a theorem's > comment. >
Definitions are opaque in Metamath - that's a restriction which was part of the language from the beginning. And that prevents automatic unfolding of definitions using definitional equivalence. It's possible to do just that using conventions and external tools, but we don't have it at the moment. Mario probably could express more authoritative opinion, especially in light of his work on MM0. N.B. Yes, such technical details affect philosophical goals after all and must be taken into account. -- 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/3fc7e623-798b-4ffc-83c6-e50976e46772%40googlegroups.com.
