Struct NegativeControl 

pub struct NegativeControl {
    pub negation_source: String,
    pub negation_name: String,
}

Negation manifest for the negative-control guard.

TODO(loop-phase): the loop must supply the formal negation of the claim so the guard can compile it and require failure. Until then this type is the wiring seam and check_negative_control is a documented no-op.

Fields

negation_source: String

Lean source for the sibling declaration asserting the negation.

negation_name: String

Name of the negation declaration.

Trait Implementations

impl Clone for NegativeControl

fn clone(&self) -> NegativeControl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NegativeControl

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

Formats the value using the given formatter.

impl Eq for NegativeControl

impl PartialEq for NegativeControl

fn eq(&self, other: &NegativeControl) -> 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 StructuralPartialEq for NegativeControl