Enum Reducibility 

pub enum Reducibility {
    Reducible,
    Semireducible,
    Irreducible,
}

Lean’s reducibility axis, declared per constant — Context::is_irreducible is the predicate reduction::Transparency::Excluding is looking for. Lean’s REDUCIBILITY axis, declared per constant and read by the elaborator’s δ step.

Three settings and not two, because @[reducible] is not merely “the default”: instance resolution unfolds a reducible definition and stops at a semireducible one, so collapsing the two changes which instances are found.

Variants

Reducible

@[reducible] — an abbreviation, unfolded even where the elaborator is being careful.

Semireducible

The default: unfolded at ordinary transparency.

Irreducible

@[irreducible] — the elaborator never unfolds it, and secret = 5 is not rfl. The body is KEPT: this is opacity, not an axiom, and the difference is that a later unfold/decide can still reach the definition.

Trait Implementations

impl Clone for Reducibility

fn clone(&self) -> Reducibility

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Reducibility

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

Formats the value using the given formatter.

impl Default for Reducibility

fn default() -> Reducibility

Returns the “default value” for a type.

impl PartialEq for Reducibility

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

impl Eq for Reducibility

impl StructuralPartialEq for Reducibility