I can go along with this. My first question is, how will it be checked? Can the mmj2 definition check be modified to ensure it?
Norm On Friday, June 14, 2019 at 8:55:10 AM UTC-4, Mario Carneiro wrote: > > Hi All, > > This is a fairly irrelevant looking change, but it does affect most of the > library as well as the mathboxes, so I would like to RFC it for a bit. In > an attempt to make definitions clearer and avoid ordering ambiguities, I > would like to institute a convention that each definition comes directly > after the constant it introduces. So we have > > $( Text text. $) > cfoo $a class foo $. > > $( Text text. $) > df-foo $a |- foo = ( x e. bar |-> x ) $. > > but the following would not be allowed: > > $( Text text. $) > cfoo $a class foo $. > > $( Text text. $) > cbar $a class bar $. > > $( Text text. $) > df-bar $a |- bar = ( x e. foo |-> x ) $. > > $( Text text. $) > df-foo $a |- foo = ( x e. bar |-> x ) $. > > I used circular definitions here to make the problem obvious, but the > basic issue is the ambiguity of definition ordering when metamath has no > innate notion of "a definition" as a unified whole. Spreading the > definition across many statements makes the problem even worse. If I see a > constant, how far forward do I need to scan to find out whether this is > actually a definition? The mmj2 definition checker uses the location of the > term constructor to determine the valid dependencies in the definitions, > but it has to scan forward arbitrarily to find the definitions. > > The solution proposed here is light-weight: just put the df-foo > immediately after foo with no intervening statements. Any syntax axiom not > followed by a definition axiom is considered to be a primitive term > constructor. > > Currently, we use a combination of term/def pairs like this, and > term/term/term/def/def/def style in larger sections. I haven't looked in > detail at the mathboxes, but I believe the story is similar. I don't think > term and def are separated by more than a section anywhere in set.mm, and > it is rare for theorems to appear in the section header area, so I expect > there will be no effect on proofs. > > Mario > -- 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/9555adc4-39e9-4b94-aa6c-2cc9e9ca29ee%40googlegroups.com.
