opaque Lean.deprecatedAttr : Lean.ParametricAttribute (Option Lean.Name)

def Lean.isDeprecated (env : Lean.Environment) (declName : Lean.Name) : Bool

Equations

• Lean.isDeprecated env declName = Option.isSome (Lean.ParametricAttribute.getParam? Lean.deprecatedAttr env declName)

def Lean.MessageData.isDeprecationWarning (msg : Lean.MessageData) : Bool

Equations

• Lean.MessageData.isDeprecationWarning msg = Lean.MessageData.hasTag (fun a => a == Lean.Name.mkStr2 "Lean" "deprecatedAttr") msg

def Lean.getDeprecatedNewName (env : Lean.Environment) (declName : Lean.Name) : Option Lean.Name

Equations

• Lean.getDeprecatedNewName env declName = match Lean.ParametricAttribute.getParam? Lean.deprecatedAttr env declName with | some newName? => newName? | none => none

def Lean.checkDeprecated {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadLog m] [inst : Lean.AddMessageContext m] [inst : Lean.MonadOptions m] (declName : Lean.Name) : m Unit

Equations

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