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/CAFXXJSvyWRiaqU0bUv%3DbhxciUZogRMQQGim6cLbFFuJ76K9aow%40mail.gmail.com.
