Enum mm0b_parser::StmtCmd

pub enum StmtCmd {
    Sort,
    Axiom,
    TermDef {
        local: bool,
    },
    Thm {
        local: bool,
    },
}

The main part of the proof consists of a sequence of declarations, and these commands denote the different kind of declaration that can be introduced.

Variants

Sort

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

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.

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

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

local: bool

Is this not pub theorem?

Implementations

impl StmtCmd

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 StmtCmd

fn clone(&self) -> StmtCmd

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for StmtCmd

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

Formats the value using the given formatter.

impl TryFrom<u8> for StmtCmd

type Error = ParseError

The type returned in the event of a conversion error.

fn try_from(cmd: u8) -> Result<Self, Self::Error>

Performs the conversion.

impl Copy for StmtCmd