Struct Not 

pub struct Not<P> {
    pub message: String,
    /* private fields */
}

A negation proof: evidence that P does not hold.

Wraps an explanatory message at the Rust meta-level.

Fields

message: String

Message explaining why P is false.

Implementations

impl<P> Not<P>

pub fn new(message: impl Into<String>) -> Self

Construct a negation proof with the given message.

pub fn message(&self) -> &str

Double negation elimination: ¬¬P is not constructively valid in general, but we model it here as just returning the message.

Trait Implementations

impl<P: Clone> Clone for Not<P>

fn clone(&self) -> Not<P>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<P: Debug> Debug for Not<P>

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

Formats the value using the given formatter.

impl<P: PartialEq> PartialEq for Not<P>

fn eq(&self, other: &Not<P>) -> bool

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<P: Eq> Eq for Not<P>

impl<P> StructuralPartialEq for Not<P>