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.
