Enum dedukti_parse::Intro
source · [−]pub enum Intro<Ty, Tm = Ty> {
Definition(Option<Ty>, Option<Tm>),
Theorem(Ty, Tm),
Declaration(Ty),
}
Expand description
A command that introduces a new constant.
Variants
Definition(Option<Ty>, Option<Tm>)
Theorem(Ty, Tm)
Declaration(Ty)
Implementations
Trait Implementations
Auto Trait Implementations
impl<Ty, Tm> RefUnwindSafe for Intro<Ty, Tm> where
Tm: RefUnwindSafe,
Ty: RefUnwindSafe,
impl<Ty, Tm> Send for Intro<Ty, Tm> where
Tm: Send,
Ty: Send,
impl<Ty, Tm> Sync for Intro<Ty, Tm> where
Tm: Sync,
Ty: Sync,
impl<Ty, Tm> Unpin for Intro<Ty, Tm> where
Tm: Unpin,
Ty: Unpin,
impl<Ty, Tm> UnwindSafe for Intro<Ty, Tm> where
Tm: UnwindSafe,
Ty: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more