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

Equations

• Lean.instInhabitedReducibilityStatus.default = Lean.ReducibilityStatus.reducible

@[implicit_reducible]

instance Lean.instInhabitedReducibilityStatus : Inhabited ReducibilityStatus

Equations

• Lean.instInhabitedReducibilityStatus = { default := Lean.instInhabitedReducibilityStatus.default }

@[implicit_reducible]

instance Lean.instReprReducibilityStatus : Repr ReducibilityStatus

Equations

• Lean.instReprReducibilityStatus = { reprPrec := Lean.instReprReducibilityStatus.repr }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.instBEqReducibilityStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Lean.instBEqReducibilityStatus : BEq ReducibilityStatus

Equations

• Lean.instBEqReducibilityStatus = { beq := Lean.instBEqReducibilityStatus.beq }

def Lean.ReducibilityStatus.toAttrString : ReducibilityStatus → String

Equations

• Lean.ReducibilityStatus.reducible.toAttrString = "[reducible]"
• Lean.ReducibilityStatus.irreducible.toAttrString = "[irreducible]"
• Lean.ReducibilityStatus.semireducible.toAttrString = "[semireducible]"
• Lean.ReducibilityStatus.implicitReducible.toAttrString = "[implicit_reducible]"

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Lean.getReducibilityStatus declName = do let __do_lift ← Lean.getEnv pure (Lean.getReducibilityStatusCore __do_lift declName)

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

Set the reducibility attribute for the given declaration.

Equations

• Lean.setReducibilityStatus declName s = Lean.modifyEnv fun (env : Lean.Environment) => Lean.setReducibilityStatusCore✝ env declName s Lean.AttributeKind.global Lean.Name.anonymous

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

Set the given declaration as [reducible]

Equations

• Lean.setReducibleAttribute declName = Lean.setReducibilityStatus declName Lean.ReducibilityStatus.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].

Equations

• Lean.isReducible declName = do let __do_lift ← Lean.getReducibilityStatus declName pure (match __do_lift with | Lean.ReducibilityStatus.reducible => true | x => false)

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]

Equations

• Lean.isIrreducible declName = do let __do_lift ← Lean.getReducibilityStatus declName pure (match __do_lift with | Lean.ReducibilityStatus.irreducible => true | x => false)

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

Equations

• Lean.isImplicitReducibleCore env declName = match Lean.getReducibilityStatusCore env declName with | Lean.ReducibilityStatus.implicitReducible => true | x => false

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].

Equations

• Lean.isImplicitReducible declName = do let __do_lift ← Lean.getEnv pure (Lean.isImplicitReducibleCore __do_lift declName)

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

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

Equations

• Lean.isInstanceReducibleCore = Lean.isImplicitReducibleCore

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

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

Equations

• @Lean.isInstanceReducible = @Lean.isImplicitReducible

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

Set the given declaration as [irreducible]

Equations

• Lean.setIrreducibleAttribute declName = Lean.setReducibilityStatus declName Lean.ReducibilityStatus.irreducible