Enum QuotReductionKind 

pub enum QuotReductionKind {
    Lift,
    Ind,
    Sound,
}

Kind of a quotient reduction rule.

Variants

Lift

Quot.lift f h (Quot.mk a) → f a.

Ind

Quot.ind h (Quot.mk a) → h a.

Sound

Quot.sound h → Quot.mk a = Quot.mk b (when r a b).

Implementations

impl QuotReductionKind

pub fn description(&self) -> &'static str

Human-readable description.

Trait Implementations

impl Clone for QuotReductionKind

fn clone(&self) -> QuotReductionKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for QuotReductionKind

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

Formats the value using the given formatter.

impl PartialEq for QuotReductionKind

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

impl StructuralPartialEq for QuotReductionKind