Enum StatementType

pub enum StatementType {
    Eof,
    Invalid,
    Comment,
    TypesettingComment,
    HeadingComment(HeadingLevel),
    AdditionalInfoComment,
    FileInclude,
    Axiom,
    Provable,
    Essential,
    Floating,
    Disjoint,
    OpenGroup,
    CloseGroup,
    Constant,
    Variable,
}

An enumeration of statement types, most of which correspond to statements as defined in the Metamath spec.

Variants

Eof

Psuedo statement used only to record end-of-file whitespace.

Invalid

Statement which is damaged enough that there’s no sense passing it to later stages.

Comment

Comments between statements are recorded as statements in their own right to facilitate handling of date comments and other metadata.

TypesettingComment

A comment which starts with a $t token and must be interpreted specially by the HTML generator.

HeadingComment(HeadingLevel)

A comment corresponding to the head of a chapter or section in the outline

AdditionalInfoComment

A comment which starts with a $j token and must be interpreted specially by the grammar parser

FileInclude

A $[ directive; we process these as statements, and disallow them inside other statements, which violates the published Metamath spec but is allowed behavior as an erratum.

Such statements always end the current segment.

Axiom

A spec $a statement.

Provable

A spec $p statement.

Essential

A spec $e statement.

Floating

A spec $f statement.

Disjoint

A spec $d statement.

OpenGroup

A spec ${ statement.

CloseGroup

A spec $} statement.

Constant

A spec $c statement.

Variable

A spec $v statement.

Implementations

impl StatementType

pub const fn is_assertion(self) -> bool

Returns true if this statement is an Axiom ($a) or Provable ($p) statement.

pub const fn takes_label(self) -> bool

Returns true if this statement has a label before the keyword: $a $p $e $f.

pub const fn takes_math(self) -> bool

Returns true if this statement is followed by math tokens: $a $p $e $f $d $c $v.

Trait Implementations

impl Clone for StatementType

fn clone(&self) -> StatementType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for StatementType

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for StatementType

fn default() -> StatementType

Returns the “default value” for a type.

impl PartialEq for StatementType

fn eq(&self, other: &StatementType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for StatementType

impl Eq for StatementType

impl StructuralPartialEq for StatementType