Enum TacticError 

pub enum TacticError {
    NoOpenGoals,
    DoesNotApply(String),
    NoSuchHypothesis(String),
    AutoFailed,
    GoalsRemain(usize),
}

What went wrong applying a tactic.

Variants

NoOpenGoals

No focused goal — the proof state is already complete.

DoesNotApply(String)

The tactic does not apply to the focused goal’s shape (e.g. intro on an atom).

NoSuchHypothesis(String)

No hypothesis (or premise) matches the goal for assumption/exact.

AutoFailed

The backward chainer could not close the goal.

GoalsRemain(usize)

qed was called with goals still open.

Trait Implementations

impl Clone for TacticError

fn clone(&self) -> TacticError

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TacticError

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

Formats the value using the given formatter.

impl PartialEq for TacticError

fn eq(&self, other: &TacticError) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for TacticError