Enum debug_sat::Proof

pub enum Proof {
    True,
    False,
    Unknown,
    Unexpected,
    Error,
}

Stores result of a proof.

Variants

True

Locally correct and no contradiction so far. NB! This does not mean that the proof is correct. This required assigning a value to every variable.

False

Contradiction. There exists some assumption of consequence of assumptions which contradicts the conclusion of the tactic.

Unknown

It is unknown whether the tactic can be applied at this moment. Add more assumptions and try again, or try a different tactic.

Unexpected

A contradiction to the assumption of the tactic was found. This does not mean the proof is wrong, but that this particular tactic is the wrong strategy.

Error

This tactic can not be performed on this expression. Usually due to grammatical error.

Trait Implementations

impl Eq for Proof

impl PartialEq for Proof

fn eq(&self, __arg_0: &Proof) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl Copy for Proof

impl Clone for Proof

fn clone(&self) -> Proof

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Proof

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl From<bool> for Proof

fn from(val: bool) -> Proof

Performs the conversion.