I realize that it seems especially inconvenient that moving df-gsum back requires moving df-0g back too. But this better reflects the reality, because df-gsum not allowed to refer to constants defined after cgsum anyway (to prevent cycles), and placing df-gsum much further along just makes this policy more unintuitive (because normally we can refer to anything before the current line).
That said, I think it would still be better to move all definitions needed for df-prds before it. This is a downside of the "everything structure" approach, but it does not displace too many definitions. We can keep the real theorems about them (including the definitional theorem) in their proper place. Mario On Thu, Feb 13, 2020, 2:44 AM 'Alexander van der Vekens' via Metamath < metamath@googlegroups.com> wrote: > 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/533047c1-210c-4a5f-aad2-cfb291f2a58a%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/533047c1-210c-4a5f-aad2-cfb291f2a58a%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvxF9_L23u8xOf93n2uTZ796KbLBtKbQHw2oDSE9NKu4w%40mail.gmail.com.
