Enum mm0b_parser::NumdStmtCmd [−][src]
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
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
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
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
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
Implementations
impl NumdStmtCmd
[src]
#[must_use]pub fn is_local(self) -> bool
[src]
Is this a “local” command, i.e. it does not appear in the corresponding MM0 file?
Trait Implementations
impl Clone for NumdStmtCmd
[src]
fn clone(&self) -> NumdStmtCmd
[src]
pub fn clone_from(&mut self, source: &Self)
1.0.0[src]
impl Copy for NumdStmtCmd
[src]
impl Debug for NumdStmtCmd
[src]
Auto Trait Implementations
impl RefUnwindSafe for NumdStmtCmd
impl Send for NumdStmtCmd
impl Sync for NumdStmtCmd
impl Unpin for NumdStmtCmd
impl UnwindSafe for NumdStmtCmd
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,