Documentation

Lean.ReducibilityAttrs

inductive Lean.ReducibilityStatus :

Type

instance Lean.instInhabitedReducibilityStatus :

Inhabited Lean.ReducibilityStatus

Equations

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

instance Lean.instReprReducibilityStatus :

Repr Lean.ReducibilityStatus

Equations

Lean.instReprReducibilityStatus = { reprPrec := [anonymous] }

constant Lean.reducibilityAttrs :

Lean.EnumAttributes Lean.ReducibilityStatus

def Lean.getReducibilityStatusImp (env : Lean.Environment) (declName : Lean.Name) :

Lean.ReducibilityStatus

Equations

Lean.getReducibilityStatusImp env declName = match Lean.EnumAttributes.getValue Lean.reducibilityAttrs env declName with | some s => s | none => Lean.ReducibilityStatus.semireducible

def Lean.setReducibilityStatusImp (env : Lean.Environment) (declName : Lean.Name) (s : Lean.ReducibilityStatus) :

Lean.Environment

Equations

Lean.setReducibilityStatusImp env declName s = match Lean.EnumAttributes.setValue Lean.reducibilityAttrs env declName s with | Except.ok env => env | x => env

def Lean.getReducibilityStatus {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

m Lean.ReducibilityStatus

Equations

Lean.getReducibilityStatus declName = do let a ← Lean.getEnv pure (Lean.getReducibilityStatusImp a declName)

def Lean.setReducibilityStatus {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) (s : Lean.ReducibilityStatus) :

Equations

Lean.setReducibilityStatus declName s = Lean.modifyEnv fun env => Lean.setReducibilityStatusImp env declName s

def Lean.setReducibleAttribute {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

Equations

Lean.setReducibleAttribute declName = Lean.setReducibilityStatus declName Lean.ReducibilityStatus.reducible

def Lean.isReducible {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

Equations

Lean.isReducible declName = do let a ← Lean.getReducibilityStatus declName match a with | Lean.ReducibilityStatus.reducible => pure true | x => pure false

def Lean.isIrreducible {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] (declName : Lean.Name) :

Equations

Lean.isIrreducible declName = do let a ← Lean.getReducibilityStatus declName match a with | Lean.ReducibilityStatus.irreducible => pure true | x => pure false