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.
• instanceReducible: Unfolded at TransparencyMode.instances or above. Auto-applied by the instance command and to subobject projections of class parents. The attribute [instance_reducible] marks a definition with this status; users typically do not need to apply it manually.
• implicitReducible: Unfolded at TransparencyMode.implicit or above (strictly above .instances). Used for definitions that should unfold when checking implicit and instance-implicit arguments for definitional equality, including for resolving instance diamonds, but must stay opaque to type class search. The attribute [implicit_reducible] marks a definition with this status. (Note: core arithmetic such as Nat.add and Array.size is deliberately instanceReducible, not implicitReducible, because type class synthesis depends on it unfolding.)
• 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
• instanceReducible : ReducibilityStatus

@[instance_reducible]

instance Lean.instInhabitedReducibilityStatus : Inhabited ReducibilityStatus

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.instReprReducibilityStatus : Repr ReducibilityStatus

Equations

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

@[instance_reducible]

instance Lean.instBEqReducibilityStatus : BEq ReducibilityStatus

Equations

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

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

Equations

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

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]"
• Lean.ReducibilityStatus.instanceReducible.toAttrString = "[instance_reducible]"

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

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

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)

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

Equations

• Lean.isInstanceReducibleCore env declName = match Lean.getReducibilityStatusCore env declName with | Lean.ReducibilityStatus.instanceReducible => true | x => false

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

Return true if the given declaration has been marked as [instance_reducible] (automatically applied by the instance command and by subobject class projections).

Equations

• Lean.isInstanceReducible declName = do let __do_lift ← Lean.getEnv pure (Lean.isInstanceReducibleCore __do_lift declName)

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