MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  conventions-comments Structured version   Visualization version   GIF version

Theorem conventions-comments 27962

The following gives conventions used in the Metamath Proof Explorer (MPE, regarding comments, and more generally nonmathematical conventions. For other conventions, see conventions 27960 and links therein.

  • Input format.

    The input format is ASCII. Tab characters are not allowed. If non-ASCII characters have to be displayed in comments, use embedded mathematical symbols when they have been defined (e.g., "` -> `" for " ") or HTML entities (e.g., "&eacute;" for "é"). Default indentation is by two spaces. Lines are hard-wrapped to be at most 79-character long, excluding the newline character (this can be achieved, except currently for section comments, by the Metamath program "MM> WRITE SOURCE / REWRAP" command or by running the script scripts/rewrap). The file ends with an empty line. There are no trailing spaces. As for line wrapping in statements, we try to break lines before the most important token.

  • Language and spelling.

    The MPE uses American English, e.g., we write "neighborhood" instead of the British English "neighbourhood". An exception is the word "analog", which can be either a noun or an adjective (furthermore, "analog" has the confounding meaning "not digital"); therefore, "analogue" is used for the noun and "analogous" for the adjective. We favor regular plurals, e.g., "formulas" instead of "formulae", "lemmas" instead of "lemmata".

    Since comments may contain many space-separated symbols, we use the older convention of two spaces after a period ending a sentence, to better separate sentences (this is also achieved by the Metamath program "MM> WRITE SOURCE / REWRAP" command).

    When compound words have several variants, we prefer the concatenated variant (e.g., nonempty, nontrivial, nonpositive, nonzero, nonincreasing, nondegenerate...).

  • Quotation style.

    We use the "logical quotation style", which means that when a quoted text is followed by punctuation not pertaining to the quote, then the quotation mark precedes the punctuation (like at the beginning of this sentence). We use the double quote as default quotation mark (since the single quote also serves as apostrophe), and the single quote in the case of a nested quotation.

  • Sectioning and section headers.

    The database has a sectioning system with four levels of titles, signaled by "decoration lines" which are 79-character long repetitions of ####, #*#*, =-=-, and -.-. (in descending order of sectioning level). Sections of any level are separated by two blank lines (if there is a "@( Begin $[ ... $] @)" comment (where "@" is actually "$") before a section header, then the double blank line should go before that comment, which is considered as belonging to that section). The format of section headers is best seen in the source file (; it is as follows:

    • a line with "@(" (with the "@" replaced by "$");
    • a decoration line;
    • section title indented with two spaces;
    • a (matching) decoration line;
    • [blank line; header comment indented with two spaces; blank line;]
    • a line with "@)" (with the "@" replaced by "$");
    • one blank line.
    As everywhere else, lines are hard-wrapped to be 79-character long. It is expected that in a future version, the Metamath program "MM> WRITE SOURCE / REWRAP" command will reformat section headers to automatically conform with this format.

  • Comments.

    As for formatting of the file, and in particular formatting and layout of the comments, the foremost rule is consistency. The first sections of, in particular Part 1 "Classical first-order logic with equality" can serve as a model for contributors. Some formatting rules are enforced when using the Metamath program "MM> WRITE SOURCE / REWRAP" command. Here are a few other rules, which are not enforced, but that we try to follow:

      A math string in a comment should be surrounded by space-separated backquotes on the same line, and if it is too long it should be broken into multiple adjacent math strings on multiple lines.
    • The file should have a double blank line between sections, and at no other places. In particular, there are no triple blank lines.
    • The header comments should be spaced as those of Part 1, namely, with a blank line before and after the comment, and an indentation of two spaces.
    • As of 20-Sep-2022, section comments are not rewrapped by the Metamath program "MM> WRITE SOURCE / REWRAP" command, though this is expected in a future version. Similar spacing and wrapping should be used as for other comments: double spaces after a period ending a sentence, line wrapping with line width of 79, and no trailing spaces at the end of lines.

  • Contributors.

    Each assertion (theorem, definition or axiom) has a contribution tag of the form "(Contributed by xxx, dd-Mmm-yyyy.)" (see Metamath Book, p. 142). The date cannot serve as a proof of anteriority since there is currently no formal guarantee that the date is correct (a claim of anterioty can be backed, for instance, by the uploading of a result to a public repository with verifiable date). The contributor is the first person who proved (or stated, in the case of a definition or axiom) the statement. The list of contributors appears at the beginning of

    An exception should be made if a theorem is essentially an extract or a variant of an already existing theorem, in which case the contributor should be that of the statement from which it is derived, with the modification signaled by a "(Revised by xxx, dd-Mmm-yyyy.)" tag.

  • Usage of parentheticals.

    Usually, the comment of a theorem should contain at most one of the "Revised by" and "Proof shortened by" parentheticals, see Metamath Book, pp. 142-143 (there must always be a "Contributed by" parenthetical for every theorem). Exceptions for "Proof shortened by" parentheticals are essential additional shortenings by a different person. If a proof is shortened by the same person, the date within the "Proof shortened by" parenthetical should be updated only. This also holds for "Revised by" parentheticals, except that also more than one of such parentheticals for the same person are acceptable (if there are good reasons for this). A revision tag is optionally preceded by a short description of the revision. Since this is somewhat subjective, judgment and intellectual honesty should be applied, with collegial settlement in case of dispute.

  • Explaining new labels.

    A comment should explain the first use of an abbreviation within a label. This is often in a definition (e.g., the definition df-an 388 introduces the abbreviation "an" for conjunction ("and")), but not always (e.g., the theorem alim 1773 introduces the abbreviation "al" for the universal quantifier ("for all")). See conventions-labels 27961 for a table of abbreviations.

(Contributed by the Metamath team, 27-Dec-2016.) Date of last revision. (Revised by the Metamath team, 22-Sep-2022.) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
conventions-comments.1 𝜑
Ref Expression
conventions-comments 𝜑

Proof of Theorem conventions-comments
StepHypRef Expression
1 conventions-comments.1 1 𝜑
Colors of variables: wff setvar class
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator