source
inductive Lean.ReducibilityStatus :
Type

Reducibility status for a definition.

- reducible : ReducibilityStatus
- semireducible : ReducibilityStatus
- irreducible : ReducibilityStatus

Instances For

source
def Lean.instInhabitedReducibilityStatus.default :
ReducibilityStatus
Equations

- Lean.instInhabitedReducibilityStatus.default = Lean.ReducibilityStatus.reducible

Instances For

source
instance Lean.instInhabitedReducibilityStatus :
Inhabited ReducibilityStatus
Equations

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

source
instance Lean.instReprReducibilityStatus :
Repr ReducibilityStatus
Equations

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

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

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

Instances For

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

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

Instances For

source
instance Lean.instBEqReducibilityStatus :
BEq ReducibilityStatus
Equations

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

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

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

Instances For

source
opaque Lean.reducibilityCoreExt :
PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus)
source
opaque Lean.reducibilityExtraExt :
SimpleScopedEnvExtension (Name × ReducibilityStatus) (SMap Name ReducibilityStatus)
source
@[export lean_get_reducibility_status]
def Lean.getReducibilityStatusCore (env : Environment) (declName : Name) :
ReducibilityStatus
Equations

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

Instances For

source
opaque Lean.allowUnsafeReducibility :
Lean.Option Bool
source
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)

Instances For

source
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

Instances For

source
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

Instances For

source
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 match __do_lift with | Lean.ReducibilityStatus.reducible => pure true | x => pure false

Instances For

source
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 match __do_lift with | Lean.ReducibilityStatus.irreducible => pure true | x => pure false

Instances For

source
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

Instances For