inductive Lean.ReducibilityStatus : Type

Reducibility status for a definition. Controls when isDefEq and whnf are allowed to unfold it. See TransparencyMode for the full design rationale.

• reducible: Unfolded at TransparencyMode.reducible or above. Reducible definitions still appear in user-facing terms, but are eagerly unfolded when indexing terms into discrimination trees (simp, type class resolution) and in grind. Think of it as [inline] for indexing. Suitable for abbreviations and definitions that should be transparent to proof automation.
• implicitReducible: Unfolded at TransparencyMode.instances or above. Used for type class instances and definitions that appear in types matched during implicit argument resolution (e.g., Nat.add, Array.size). These definitions cannot be eagerly reduced (instances expand into large terms, recursive definitions are problematic), but must be unfoldable when checking implicit arguments and resolving instance diamonds (e.g., Add Nat via direct instance vs via Semiring). The attribute [implicit_reducible] (or its alias [instance_reducible]) marks a definition with this status.
• semireducible: The default. Unfolded at TransparencyMode.default or above. Used for ordinary definitions. Suitable for user-written code where isDefEq should try hard during type checking, but not during speculative proof automation.
• irreducible: Only unfolded at TransparencyMode.all. The definition body is effectively hidden from isDefEq in normal usage.

• reducible : ReducibilityStatus
• semireducible : ReducibilityStatus
• irreducible : ReducibilityStatus
• implicitReducible : ReducibilityStatus

def Lean.instInhabitedReducibilityStatus.default : ReducibilityStatus

@[implicit_reducible]

instance Lean.instInhabitedReducibilityStatus : Inhabited ReducibilityStatus

@[implicit_reducible]

instance Lean.instReprReducibilityStatus : Repr ReducibilityStatus

def Lean.instReprReducibilityStatus.repr : ReducibilityStatus → Nat → Format

def Lean.instBEqReducibilityStatus.beq : ReducibilityStatus → ReducibilityStatus → Bool

@[implicit_reducible]

instance Lean.instBEqReducibilityStatus : BEq ReducibilityStatus

def Lean.ReducibilityStatus.toAttrString : ReducibilityStatus → String

opaque Lean.reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus)

opaque Lean.reducibilityExtraExt : SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus)

@[export lean_get_reducibility_status]

def Lean.getReducibilityStatusCore (env : Environment) (declName : Name) : ReducibilityStatus

opaque Lean.allowUnsafeReducibility : Lean.Option Bool

def Lean.getReducibilityStatus {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus

Return the reducibility attribute for the given declaration.

def Lean.setReducibilityStatus {m : Type → Type} [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit

Set the reducibility attribute for the given declaration.

def Lean.setReducibleAttribute {m : Type → Type} [MonadEnv m] (declName : Name) : m Unit

Set the given declaration as [reducible]

def Lean.isReducible {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m Bool

Return true if the given declaration has been marked as [reducible].

def Lean.isIrreducible {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m Bool

Return true if the given declaration has been marked as [irreducible]

def Lean.isImplicitReducibleCore (env : Environment) (declName : Name) : Bool

def Lean.isImplicitReducible {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m Bool

Return true if the given declaration has been marked as [implicit_reducible].

@[reducible, inline, deprecated Lean.isImplicitReducibleCore (since := "2026-02-18")]

abbrev Lean.isInstanceReducibleCore (env : Environment) (declName : Name) : Bool

@[reducible, inline, deprecated Lean.isImplicitReducible (since := "2026-02-18")]

abbrev Lean.isInstanceReducible {m : Type → Type} [Monad m] [MonadEnv m] (declName : Name) : m Bool

def Lean.setIrreducibleAttribute {m : Type → Type} [MonadEnv m] (declName : Name) : m Unit

Set the given declaration as [irreducible]