pub enum LogicRun {
Theorem(Result<TheoremCompileResult, String>),
Sentences(CompileResult, ProofCompileResult),
Empty,
}Expand description
What running a Logic document produced.
Variants§
Theorem(Result<TheoremCompileResult, String>)
A ## Theorem: block: its compiled result, or why it did not compile.
Sentences(CompileResult, ProofCompileResult)
Plain sentences: their readings, and the first of them compiled for the prover.
Empty
Nothing but headers and comments.
Auto Trait Implementations§
impl Freeze for LogicRun
impl RefUnwindSafe for LogicRun
impl Send for LogicRun
impl Sync for LogicRun
impl Unpin for LogicRun
impl UnsafeUnpin for LogicRun
impl UnwindSafe for LogicRun
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T> Downcast for Twhere
T: Any,
impl<T> Downcast for Twhere
T: Any,
§fn into_any(self: Box<T>) -> Box<dyn Any>
fn into_any(self: Box<T>) -> Box<dyn Any>
Convert
Box<dyn Trait> (where Trait: Downcast) to Box<dyn Any>. Box<dyn Any> can
then be further downcast into Box<ConcreteType> where ConcreteType implements Trait.§fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
Convert
Rc<Trait> (where Trait: Downcast) to Rc<Any>. Rc<Any> can then be
further downcast into Rc<ConcreteType> where ConcreteType implements Trait.§fn as_any(&self) -> &(dyn Any + 'static)
fn as_any(&self) -> &(dyn Any + 'static)
Convert
&Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &Any’s vtable from &Trait’s.§fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
Convert
&mut Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &mut Any’s vtable from &mut Trait’s.§impl<T> DowncastSync for T
impl<T> DowncastSync for T
§impl<T> InitializeFromFunction<T> for T
impl<T> InitializeFromFunction<T> for T
§fn initialize_from_function(f: fn() -> T) -> T
fn initialize_from_function(f: fn() -> T) -> T
Create an instance of this type from an initialization function
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
§impl<T, O> SuperFrom<T> for Owhere
O: From<T>,
impl<T, O> SuperFrom<T> for Owhere
O: From<T>,
§fn super_from(input: T) -> O
fn super_from(input: T) -> O
Convert from a type to another type.
§impl<T, O, M> SuperInto<O, M> for Twhere
O: SuperFrom<T, M>,
impl<T, O, M> SuperInto<O, M> for Twhere
O: SuperFrom<T, M>,
§fn super_into(self) -> O
fn super_into(self) -> O
Convert from a type to another type.