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/CAFXXJSvN6zCmsZ4uLzJqfmPPjuAs1fp53cKL9%2BqEYGsYzktTHg%40mail.gmail.com.
