Reducibility status for a definition.
- reducible : ReducibilityStatus
- semireducible : ReducibilityStatus
- irreducible : ReducibilityStatus
Instances For
Equations
Equations
- Lean.instReprReducibilityStatus = { reprPrec := Lean.reprReducibilityStatus✝ }
Equations
@[export lean_get_reducibility_status]
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.setReducibilityStatus
{m : Type → Type}
[MonadEnv m]
(declName : Name)
(s : ReducibilityStatus)
:
m Unit
Set the reducibility attribute for the given declaration.
Equations
Instances For
Set the given declaration as [reducible]
Equations
Instances For
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
Instances For
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
Instances For
Set the given declaration as [irreducible]