Enum CongrArgKind 

pub enum CongrArgKind {
    Fixed,
    Eq,
    HEq,
    Cast,
    Subsingle,
}

Kind of congruence argument.

When generating a congruence lemma for f a₁ a₂ ... aₙ, each argument aᵢ falls into one of these categories.

Variants

Fixed

Fixed: this argument is the same on both sides (e.g., type parameters).

Eq

Eq: this argument requires an equality proof aᵢ = bᵢ.

HEq

HEq: this argument requires a heterogeneous equality HEq aᵢ bᵢ.

Cast

Cast: this argument is obtained by casting via a previous equality.

Subsingle

Subsingletonality: this argument is in a subsingleton type (at most one element), so any two values are equal.

Trait Implementations

impl Clone for CongrArgKind

fn clone(&self) -> CongrArgKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CongrArgKind

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

Formats the value using the given formatter.

impl PartialEq for CongrArgKind

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

impl Eq for CongrArgKind

impl StructuralPartialEq for CongrArgKind