- reducible: Lean.ReducibilityStatus
- semireducible: Lean.ReducibilityStatus
- irreducible: Lean.ReducibilityStatus
Reducibility status for a definition.
Instances For
Environment extension for storing the reducibility attribute for definitions.
def
Lean.getReducibilityStatus
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
(declName : Lake.Name)
:
Return the reducibility attribute for the given declaration.
Instances For
def
Lean.setReducibilityStatus
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
(declName : Lake.Name)
(s : Lean.ReducibilityStatus)
:
m Unit
Set the reducibility attribute for the given declaration.
Instances For
def
Lean.setReducibleAttribute
{m : Type → Type}
[Monad m]
[Lean.MonadEnv m]
(declName : Lake.Name)
:
m Unit
Set the given declaration as [reducible]
Instances For
Return true
if the given declaration has been marked as [reducible]
.
Instances For
Return true
if the given declaration has been marked as [irreducible]