No, there are more rules than just that. I'm sure I've posted about this on the group before but the best link I can find at the moment is https://groups.google.com/g/metamath/c/HdfvWF2WhBE/m/bqL0Q7E_BQAJ . The "definition" $j command is rarely used; it is only there to help parse a definitional axiom as preparation for running the actual definition check. Most of the time, the structure of the definition is manifest, because it is an equality of some kind (like `<->`) with the defined symbol on the left and the body of the definition on the right. Once these parts are identified, it is possible to check the definition rules; in your example the "definition" ~ancom would be rejected because the defined symbol `/\` occurs in the definition body.
On Sun, Nov 13, 2022 at 5:54 PM Zheng Fan <[email protected]> wrote: > In the document on the $j comments, it says that "The definition should > have a top level equality declared by the <code>equality</code> command > with the definition on the right hand side," except for df-bi. Is this > condition sufficient for a definition? For example, we have the theorem > > ancom $p |- ( ( ph /\ ps ) <-> ( ps /\ ph ) ) $= ... $. > > It also has a top level equality (<->) for wff, but it is not a definition > for /\. > > 在2022年11月13日星期日 UTC+1 02:44:32<[email protected]> 写道： > >> On Sat, Nov 12, 2022 at 7:10 PM Zheng Fan <[email protected]> wrote: >> >>> I haven't paid a lot of attention to the $j comments. I was under the >>> impression from the official specs that comments are mostly ignored. >>> Anyway, is there any specs about the meaning of the $j comments? And which >>> part of the program (if any) is responsible for parsing the $j comments? >>> And what does unambiguous 'klr 5' mean? >>> >> >> It's not yet up on the website (cc: David), but >> https://github.com/metamath/set.mm/blob/develop/j-commands.html has some >> documentation on the meaning of all the $j commands. The purpose of the >> commands is to make the various "conventions" around metamath database >> naming and interpretation of axioms more formalized and machine-checkable, >> so it is particularly of interest to metamath-knife. The $j commands are >> ignored by metamath verifiers, but it still has relevant information for >> tools that want to do more than simply verify the database; in particular >> it is relevant for parsing the statements and identifying definitions (as >> distinct from axioms) and verifying conservativity. >> >> In metamath-knife, the case that handles parsing $t and $j commands is: >> >> https://github.com/david-a-wheeler/metamath-knife/blob/614c3527fe79206e12eaa633d4c7561736cbb9fd/src/parser.rs#L747-L758 >> which defers to CommandIter which does the low level parsing. (Parsing $t >> and $j commands is a bit more difficult than the rest of it since it has >> more C-like lexing rules, which allow you to omit spaces before `;` and >> such.) The parsing of $t comments is also described in the Metamath book, >> and $j commands use the same parser. >> . >> After parsing the broad structure of the $j command, the result is >> stashed in Segment.j_commands, and further interpretation is done on the >> fly as required by individual analysis passes. The most important $j >> command which is read by almost every parser that makes an attempt to read >> $j commands at all is "syntax"; this tells you the information that you >> were asking about - that theorems start with "|-" and "wff" is the typecode >> for formulas. It is parsed by the Grammar module at: >> >> https://github.com/david-a-wheeler/metamath-knife/blob/071292ef3a10350d0dae9e409b4921f91a08ce95/src/grammar.rs#L417-L433 >> >> The "unambiguous" command is used to signal that grammatical parsing is >> possible at all. The 'klr 5' indicates more specifically that a KLR parser >> table can be built, which is one way to verify that the grammar is in fact >> unambiguous, but for most purposes it suffices just to know the mere fact >> of unambiguity (which is in general undecidable), and even then most tools >> that attempt grammatical parsing ignore the directive and simply fail or >> produce odd results on ambiguous grammars. Metamath-knife ignores this >> command. >> >> Mario >> >> 在2022年11月12日星期六 UTC+1 21:05:54<[email protected]> 写道： >>> >>>> On Sat, Nov 12, 2022 at 1:44 PM Zheng Fan <[email protected]> >>>> wrote: >>>> >>>>> if I want to add some new functions, is it better to add it to the >>>>> relevant file or create a new file? >>>>> >>>> >>>> That depends on the function. Usually a function would go in the file >>>> which defines the type on which the function is exposed, unless it is >>>> really big in which case you might consider separate files. Rust source >>>> files tend to be fairly large, they are only broken up by topic and there >>>> aren't any strict file limits. >>>> >>>> Also, do we assume the syntax of set.mm in the source code, e.g., wff >>>>> precedes a formula, |- precedes a theorem, >>>> >>>> >>>> These "conventions" are encoded in $j comments, so I would prefer to >>>> make use of that information when possible rather than hard coding them in >>>> the tool. >>>> >>>> >>>>> and the label of a definition begins with "df-"? >>>>> >>>> >>>> This one is only used in linter-like behavior, but I believe it is >>>> hard-coded. A lot of "verify markup"'s behavior is hard coded to >>>> maintenance of set.mm specifically. >>>> >>>> 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/1cbae7e9-53bf-4c83-9e23-e2bb31c965dfn%40googlegroups.com >>> <https://groups.google.com/d/msgid/metamath/1cbae7e9-53bf-4c83-9e23-e2bb31c965dfn%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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/c2cd90b8-fb09-40fb-8e5a-4ffbb3e1d042n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/c2cd90b8-fb09-40fb-8e5a-4ffbb3e1d042n%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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvQmzWbc26LzcMy0-ahtfTgHJJYFCwb9BUgEAk7rHGDWA%40mail.gmail.com.
