pub enum ClaimStatus {
Passed,
Failed,
Vacuous,
ProvedByExhaustion,
Held,
Falsified,
Proved,
Unproved,
Assumption,
}Expand description
The honest per-item status.
Variants§
Passed
An example whose assertions all held.
Failed
An example/property whose check failed (a property failure carries a
concrete counterexample; see InventoryItem::counterexample).
Vacuous
A ## Test that RAN CLEAN but asserted NOTHING — a green that checked
nothing (the non-vacuity gate fails it; the inventory surfaces it too).
ProvedByExhaustion
A property that held over every case of a FINITE domain exhausted under
--prove — a certificate over that finite domain, NOT an unrestricted
proof (the item stays finite_enumeration: true, proof: false).
Held
A property that held over its SAMPLED cases (an infinite domain, or the
finite domain without --prove) — evidence, not a proof.
Falsified
A property with a concrete counterexample — disproved.
Proved
A theorem the proof engine kernel-certified — an actual proof.
Unproved
A theorem the proof engine could not discharge.
Assumption
An axiom / admitted assumption — a premise, reported as an assumption, explicitly not a proof.
Trait Implementations§
Source§impl Clone for ClaimStatus
impl Clone for ClaimStatus
Source§fn clone(&self) -> ClaimStatus
fn clone(&self) -> ClaimStatus
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read moreSource§impl Debug for ClaimStatus
impl Debug for ClaimStatus
Source§impl PartialEq for ClaimStatus
impl PartialEq for ClaimStatus
Source§impl Serialize for ClaimStatus
impl Serialize for ClaimStatus
impl Copy for ClaimStatus
impl Eq for ClaimStatus
impl StructuralPartialEq for ClaimStatus
Auto Trait Implementations§
impl Freeze for ClaimStatus
impl RefUnwindSafe for ClaimStatus
impl Send for ClaimStatus
impl Sync for ClaimStatus
impl Unpin for ClaimStatus
impl UnsafeUnpin for ClaimStatus
impl UnwindSafe for ClaimStatus
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
§impl<T> Downcast for Twhere
T: Any,
impl<T> Downcast for Twhere
T: Any,
§fn into_any(self: Box<T>) -> Box<dyn Any>
fn into_any(self: Box<T>) -> Box<dyn Any>
Box<dyn Trait> (where Trait: Downcast) to Box<dyn Any>. Box<dyn Any> can
then be further downcast into Box<ConcreteType> where ConcreteType implements Trait.§fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
fn into_any_rc(self: Rc<T>) -> Rc<dyn Any>
Rc<Trait> (where Trait: Downcast) to Rc<Any>. Rc<Any> can then be
further downcast into Rc<ConcreteType> where ConcreteType implements Trait.§fn as_any(&self) -> &(dyn Any + 'static)
fn as_any(&self) -> &(dyn Any + 'static)
&Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &Any’s vtable from &Trait’s.§fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
fn as_any_mut(&mut self) -> &mut (dyn Any + 'static)
&mut Trait (where Trait: Downcast) to &Any. This is needed since Rust cannot
generate &mut Any’s vtable from &mut Trait’s.§impl<T> DowncastSync for T
impl<T> DowncastSync for T
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key and return true if they are equal.