This is a snapshot of the ASCII database file "set.mm" (contained in the
Metamath program download). For
efficiency, the proofs in set.mm are typically stored in a compressed
format that is hard for humans to read directly. (But if you want to
try, the precise specification of the compressed format is given in
Appendix B, p. 157, of the Metamath
book.) The Metamath program is used to work with the proofs and can
display them in several different ways, such as the web page 2eu5, which was generated with the command
"show statement 2eu5 /html". The markup syntax for symbols, cross
references, and bibliographic references in comments is described under
the Metamath program commands "help language" and "help html".
Notes The
monospaced font in the editor screen is 8-point Andale Mono. The KEDIT
editor is a product of the Mansfield Software Group. The syntax
coloring is specified by a file called mm.kld, which is placed in
KEDIT's USER directory.
* MM.KLD - KEDIT Language Definition for .mm (Metamath) files
:case
respect
:identifier
[a-zA-Z0-9${}.=] [a-zA-Z0-9${}.=]
:comment
paired $( $) nonest
:keyword
${ ALTERNATE 9
$} ALTERNATE 9
$d ALTERNATE 1
$p ALTERNATE 1
$v ALTERNATE 1
$= ALTERNATE 1
$. ALTERNATE 1
$a ALTERNATE 1
$e ALTERNATE 1
$f ALTERNATE 1
$c ALTERNATE 1
|
If you have created Metamath syntax coloring for another editor, let
me know and I will add it here.
Here is an experimental browser for Metamath on the
Palm Tungsten E PDA:
This page was last updated on
13-Oct-2006.
Metamath