Are you referring to metamath-knife? I can't find relevant code dealing with definitions in the source.
在2022年11月14日星期一 UTC+1 01:17:39<[email protected]> 写道： > 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/a43f4e76-aacf-4394-a251-b2303811016an%40googlegroups.com.
