Interface | Description |
---|---|
ProofVerifier |
Interface to proof verification.
|
SyntaxVerifier |
Interface to Syntax Verification (aka "Grammar", "grammatical parsing" and
"syntactic analysis").
|
SystemLoader |
Interface for loading Metamath statements into a Logic System.
|
Class | Description |
---|---|
Assrt |
Assrt is an "Assertion", of which there are two main kinds, Axiom and Theorem
-- known in Metamath as "Axiomatic Assertions" and "Provable Assertions".
|
Axiom |
Axiom embodies Metamath $a statements, the "axiomatic assertions".
|
BookManager |
BookManager is a "helper" class that is used to keep track of Chapter and
Section definitions for an input Metamath database and its objects (called
"MObj"s herein.)
|
Chapter |
Chapter is a baby class that provides a way to provide a title for a grouping
of Sections.
|
Cnst |
Cnst holds a declared Metamath constant symbol.
|
DjVars |
DjVars is a simple structure that holds a pair of variables specified in a
Metamath $d statement, the "Disjoint Variable Restriction" statement.
|
Formula |
Formula is, basically just an array of Sym, with a counter.
|
Hyp |
Hyp unifies VarHyp (Variable Hypothesis) and LogHyp (Logical Hypothesis).
|
LangConstants |
Constants used in mmj.lang package.
|
LogHyp |
LogHyp -- Logical Hypothesis -- corresponds to the Metamath "$e", or
"essential hypothesis" statement.
|
LogicalSystem |
The
LogicalSystem , along with the rest of the mmj.lang
package, implements the abstract portion of the Metamath language -- the
"object" language of Metamath, as opposed to the "metalanguage" of Metamath
source files. |
Messages |
Repository of error and informational messages during mmj processing.
|
MObj |
MObj (Metamath Object) is root of Sym and Stmt.
|
ParseNode |
Parse Node is an n-way tree node for Metamath Stmt trees.
|
ParseNodeHolder |
ParseNodeHolder is either really dumb or just kinda dumb.
|
ParseTree |
A simple tree structure to hold a ParseNode root.
|
ParseTree.RPNStep |
Stores backreference information in "packed" and "compressed" formats.
|
ProofCompression |
ProofCompression provides Compression and Decompression Services for Metamath
proofs as described in Metamath(dot)pdf at metamath(dot)org.
|
ScopeDef |
This is just a simple data structure used to hold the items local to a
"scope" level in Metamath.
|
ScopeFrame |
A combined class representing
mandFrame , the Mandatory "Frame" of an
Assrt (assertion), as well as optFrame , the Optional "Frame" of a
Theorem (OptFrame not present in other Assrt's). |
Section |
Section is a rudimentary class containing information for BookManager about
the grouping of statements in a Chapter within a Metamath database.
|
SeqAssigner |
The
SeqAssigner generates sequence numbers for Metamath objects
(MObj) within the mmj2 Logical System. |
Stmt |
Stmt is the parent class of all Metamath
Hyp s (hypotheses) and
Assrt s. |
Sym |
Sym holds a declared Metamath symbol and is the base class for Cnst and Var.
|
Theorem |
Theorem corresponds to a Metamath "$p" statement, AKA, a "provable assertion"
.
|
Var |
Var holds a declared Metamath variable symbol.
|
VarHyp |
VarHyp -- Variable Hypothesis -- corresponds to the Metamath "$f" statement,
or "floating hypothesis" statement.
|
VarHypSubst | |
WorkVar | |
WorkVarHyp | |
WorkVarManager |
WorkVarManager is a "helper" class that is used to define, declare, alloc and
maintain state information about a set of Work Variables.
|
Exception | Description |
---|---|
LangException |
Thrown when Metamath source file has a non-fatal error such as a syntax
error.
|