| Description:
The following gives conventions used in the Metamath Proof Explorer
(MPE, set.mm) regarding comments, and more generally nonmathematical
conventions.
For other conventions, see conventions 28764 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., "é" 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 set.mm / 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". We use the serial comma (Oxford comma) in enumerations. We
use commas after "i.e." and "e.g.".
We avoid beginning a sentence with a symbol (for instance, by writing
"The function F is ..." instead of "F is...").
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 set.mm / 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 set.mm 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 (set.mm); 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 set.mm / REWRAP" command will reformat section headers to
automatically conform with this format.
- Comments.
As for formatting of the file set.mm, and in particular formatting and
layout of the comments, the foremost rule is consistency. The first
sections of set.mm, 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
set.mm / 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 set.mm 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 set.mm / 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 set.mm.
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., Definition df-an 397
introduces the abbreviation "an" for conjunction ("and")), but not
always (e.g., Theorem alim 1813 introduces the abbreviation "al" for
the universal quantifier ("for all")). See conventions-labels 28765 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.) |
