Documentation

Lean.Linter.Deprecated

source
opaque Lean.Linter.linter.deprecated :
Lean.Option Bool
source
opaque Lean.Linter.deprecatedAttr :
Lean.ParametricAttribute (Option Lake.Name)
source
def Lean.Linter.isDeprecated (env : Lean.Environment) (declName : Lake.Name) :
Bool
Instances For
    source
    def Lean.MessageData.isDeprecationWarning (msg : Lean.MessageData) :
    Bool
    Instances For
      source
      def Lean.Linter.getDeprecatedNewName (env : Lean.Environment) (declName : Lake.Name) :
      Option Lake.Name
      Instances For
        source
        def Lean.Linter.checkDeprecated {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadLog m] [Lean.AddMessageContext m] [Lean.MonadOptions m] (declName : Lake.Name) :
        m Unit
        Instances For