While working on Github issue #1457, <https://github.com/metamath/set.mm/issues/1457>I encountered a situation in set.mm which illustrates this topic. It is the definition of `gsum` (~df-gsum), which must be placed far before the related theorems because the symbol `gsum` is used in definition ~df-prds already. And it is not sufficient to have the constant definitions "$c gsum $." and "cgsu $a class gsum $." earlier (for metamath.exe it is, for mmj2 it isn't: mmj2 would throw an error message like "Axiom df-gsum has failed the definitional soundness check. The previous axiom df-prds uses the symbol being defined in this axiom.").
And since ~df-gsum uses `0g`, its definitions (including ~df-0g) must occur even before ~df-gsum! I think this is really awkward. There are two possible solutions: - to allow a definition (~df-...) to be placed after the usage of the corresponding symbol (and before it is really used, of course). But I think this is exactly the opposite to what Mario proposes. - to revise the definitions of ~df-prds, ~df-imas, etc. (but I do not know if this would be possible at all...) Alexander -- 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/533047c1-210c-4a5f-aad2-cfb291f2a58a%40googlegroups.com.
