Struct DefBuilder

pub struct DefBuilder<'a, W>(/* private fields */);

Expand description

An unfinished definition. The unify and proof streams should be used to write unify and proof commands, respectively, and when completed the finish function will finalize the streams and return the TermId of the new definition.

Implementations§

impl<'a, W: Reopen> DefBuilder<'a, W>

pub fn unify(&mut self) -> &mut impl Write

A reference to the unify stream for this definition. Use UnifyCmd::write_to to add commands to this stream. Do not add an END command at the end; [finish] will handle that.

pub fn proof(&mut self) -> &mut impl Write

A reference to the proof stream for this definition. Use ProofCmd::write_to to add commands to this stream. Do not add an END command at the end; [finish] will handle that.

pub fn finish(self) -> Result<TermId>

Finish the unify and proof streams for this definition, and finalize the term addition. Returns the ID of the newly created term.

Trait Implementations§

impl<'a, W: Debug> Debug for DefBuilder<'a, W>

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

Formats the value using the given formatter. Read more

Auto Trait Implementations§

impl<'a, W> Freeze for DefBuilder<'a, W>

impl<'a, W> RefUnwindSafe for DefBuilder<'a, W>
where W: RefUnwindSafe,

impl<'a, W> Send for DefBuilder<'a, W>
where W: Send,

impl<'a, W> Sync for DefBuilder<'a, W>
where W: Sync,

impl<'a, W> Unpin for DefBuilder<'a, W>

impl<'a, W> !UnwindSafe for DefBuilder<'a, W>

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.