Struct mm0b_parser::ThmBuilder

pub struct ThmBuilder<'a, W>(_, _);

An unfinished axiom or theorem. 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 ThmId of the new theorem.

Implementations

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

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

A reference to the unify stream for this theorem. 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 theorem. 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<ThmId>

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

Trait Implementations

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

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

Formats the value using the given formatter.