inductive Lean.ReducibilityStatus : Type

Reducibility status for a definition.

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

instance Lean.instInhabitedReducibilityStatus : Inhabited ReducibilityStatus

instance Lean.instReprReducibilityStatus : Repr ReducibilityStatus

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.setIrreducibleAttribute {m : Type → Type} [MonadEnv m] (declName : Name) : m Unit

Set the given declaration as [irreducible]