Enum AxiomThm 

pub enum AxiomThm<S> {
    Start {
        idx: u32,
        is_axiom: bool,
        stream: S,
    },
    RunProof {
        stepper: Stepper<S>,
        is_axiom: bool,
        commands: Range<usize>,
        nr_args: usize,
    },
    ProofDone {
        stream: S,
        is_axiom: bool,
        commands: Range<usize>,
        nr_args: usize,
    },
    RunUnify {
        stream: S,
        stepper: Stepper,
    },
    Done {
        stream: S,
    },
    Dummy,
}

Variants

Start

Fields

idx: u32

is_axiom: bool

stream: S

RunProof

Fields

stepper: Stepper<S>

is_axiom: bool

commands: Range<usize>

nr_args: usize

ProofDone

Fields

stream: S

is_axiom: bool

commands: Range<usize>

nr_args: usize

RunUnify

Fields

stream: S

stepper: Stepper

Done

Fields

stream: S

Dummy

Implementations

impl<S> AxiomThm<S>

where S: Iterator<Item = Command<Proof>>,

pub fn new(idx: u32, stream: S, is_axiom: bool) -> AxiomThm<S>

pub fn take_stream_if_done(self) -> Option<S>

pub fn is_done(&self) -> bool

pub fn step<SS: Store, T: Table<Var = SS::Var>>( &mut self, context: &mut Context<SS>, state: &State, table: &T, ) -> KResult<AxiomThmAction>

Trait Implementations

impl<S: Debug> Debug for AxiomThm<S>

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

Formats the value using the given formatter.