Enum debug_sat::Proof
[−]
[src]
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
[src]
impl PartialEq for Proof
[src]
fn eq(&self, __arg_0: &Proof) -> bool
[src]
This method tests for self
and other
values to be equal, and is used by ==
. Read more
fn ne(&self, other: &Rhs) -> bool
1.0.0[src]
This method tests for !=
.
impl Copy for Proof
[src]
impl Clone for Proof
[src]
fn clone(&self) -> Proof
[src]
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
Performs copy-assignment from source
. Read more