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?
在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.
