inductive Lean.ReducibilityStatus : Type

Reducibility status for a definition.

• reducible: Lean.ReducibilityStatus
• semireducible: Lean.ReducibilityStatus
• irreducible: Lean.ReducibilityStatus

instance Lean.instInhabitedReducibilityStatus : Inhabited Lean.ReducibilityStatus

Equations

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

instance Lean.instReprReducibilityStatus : Repr Lean.ReducibilityStatus

Equations

• Lean.instReprReducibilityStatus = { reprPrec := Lean.reprReducibilityStatus✝ }

instance Lean.instBEqReducibilityStatus : BEq Lean.ReducibilityStatus

Equations

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

def Lean.ReducibilityStatus.toAttrString : Lean.ReducibilityStatus → String

Equations

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

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

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

@[export lean_get_reducibility_status]

def Lean.getReducibilityStatusCore (env : Lean.Environment) (declName : Lean.Name) : Lean.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] [Lean.MonadEnv m] (declName : Lean.Name) : m Lean.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} [Lean.MonadEnv m] (declName : Lean.Name) (s : Lean.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} [Lean.MonadEnv m] (declName : Lean.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] [Lean.MonadEnv m] (declName : Lean.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 match __do_lift with | Lean.ReducibilityStatus.reducible => pure true | x => pure false

def Lean.isIrreducible {m : Type → Type} [Monad m] [Lean.MonadEnv m] (declName : Lean.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 match __do_lift with | Lean.ReducibilityStatus.irreducible => pure true | x => pure false

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

Set the given declaration as [irreducible]

Equations

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