On November 27, 2019 4:04:11 PM EST, 'Alexander van der Vekens' via Metamath <[email protected]> wrote: >... I do not fully agree with having more definitions in general. Definitions >should be globally meaningful, and >not only abbreviations for a single proof/theorem (or a limited group of >theorems).
Fair enough. I agree that in Metamath definitions should be more broadly useful, not something only useful a few times. I just think we sometimes shy away from creating definitions even when they *would* apply to many theorems. This appears to be an advantage of Metamath Zero, which permits local definitions (unlike straight Metamath). The newer "operation" variables of set.mm, like plus-with-broken-underline, do help. None of this is meant to take away from your success!! --- David A.Wheeler -- 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/A3F6B686-7733-49AF-B056-4BAD840CCC82%40dwheeler.com.
