Enum Intro 

pub enum Intro<Ty, Tm = Ty> {
    Definition(Option<Ty>, Option<Tm>),
    Theorem(Ty, Tm),
    Declaration(Ty),
}

A command that introduces a new constant.

Variants

Definition(Option<Ty>, Option<Tm>)

Theorem(Ty, Tm)

Declaration(Ty)

Implementations

impl<Ty, Tm> Intro<Ty, Tm>

pub fn rewritable(&self) -> bool

Only constants introduced by definitions are rewritable.

pub fn map_type<U>(self, f: impl FnOnce(Ty) -> U) -> Intro<U, Tm>

Apply a function to the type of the introduced constant, if given.

pub fn map_term<U>(self, f: impl FnOnce(Tm) -> U) -> Intro<Ty, U>

Apply a function to the term of the introduced constant, if given.

Trait Implementations

impl<Ty: Clone, Tm: Clone> Clone for Intro<Ty, Tm>

fn clone(&self) -> Intro<Ty, Tm>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<Ty: Debug, Tm: Debug> Debug for Intro<Ty, Tm>

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

Formats the value using the given formatter.