Enum mm0b_parser::NumdStmtCmd

pub enum NumdStmtCmd {
    Sort {
        sort_id: SortId,
    },
    Axiom {
        thm_id: ThmId,
    },
    TermDef {
        term_id: TermId,
        local: bool,
    },
    Thm {
        thm_id: ThmId,
        local: bool,
    },
}

StmtCmd aware of its position (represented by a typesafe integer) in the mmb file relative to other declarations.

Variants

Sort

A new sort. Equivalent to sort foo;. This is followed by no data, as the sort data is stored in the header.

Fields of Sort

sort_id: SortId

The sort ID, the index into the sort table

Axiom

A new axiom. Equivalent to axiom foo .... This is followed by a proof sequence, that should unify with the unify sequence in the header.

Fields of Axiom

thm_id: ThmId

The theorem ID, the index into the axiom/theorem table

TermDef

A new term or def. Equivalent to term/def foo .... If local is true, then this is local def foo. This is followed by no data, as the header contains the unify sequence and can be checked on its own.

Fields of TermDef

term_id: TermId

The term ID, the index into the term/def table

local: bool

Is this local def?

Thm

A new theorem. Equivalent to (pub) theorem foo ..., where local means that the theorem is not pub. This is followed by a proof sequence, that will construct the statement and proof, and should unify with the unify sequence in the header.

Fields of Thm

thm_id: ThmId

The theorem ID, the index into the axiom/theorem table

local: bool

Is this not pub theorem?

Implementations

impl NumdStmtCmd

pub fn is_local(self) -> bool

Is this a “local” command, i.e. it does not appear in the corresponding MM0 file?

Trait Implementations

impl Clone for NumdStmtCmd

fn clone(&self) -> NumdStmtCmd

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for NumdStmtCmd

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

Formats the value using the given formatter.

impl Copy for NumdStmtCmd