Crate metamath_rs

A library for manipulating Metamath databases. The entry point for all API operations is in the database module, as is a discussion of the data representation.

Re-exports

pub use database::Database;

pub use formula::Formula;

pub use formula::FormulaRef;

pub use formula::Label;

pub use formula::Symbol;

pub use parser::is_valid_label;

pub use statement::as_str;

pub use statement::Span;

pub use statement::StatementRef;

pub use statement::StatementType;

Modules

axiom_use

Generation of the axiom_use file.

comment_parser

Implements markup parsing for metamath theorem comments.

database

Main API entry point for reading and manipulating Metamath databases.

diag

Datatypes to represent diagnostics emitted by smetamath analysis passes.

discouraged

Regeneration of the discouraged file.

export

Export support for mmj2 proof files.

formula

Formula stores the result of a parsing as the tree of its “syntactic proof” The formula nodes are the equivalent of MMJ2’s ParseNodes, and the formula itself the equivalent of MMJ2’s ParseTree

grammar

Grammar processes a database, extracts a Grammar, which it also validates, and parses statements in the system.

line_cache

Utilities for source-offset/line-number mapping.

nameck

Analysis pass which builds the name to definition index.

outline

The database outline.

parser

Implementation of the low-level statement parser for Metamath databases.

proof

The proof object model for RPN proofs used in Metamath.

scopeck

This module calculates 3 things which are related only by the fact that they can be done at the same time:

statement

The Statement data structure and related API.

typesetting

The typesetting data.

verify

The proof verifier itself.

verify_markup

Verification of comment markup and other niceties for HTML generation.

Structs

SourceInfo

Tracks source information for a Segment that can be used by the diagnostic printer.

Traits

Comparer

A trait for objects which can be used to order other datatypes.