Documentation

Lean.Linter.Deprecated

source
opaque Lean.Linter.linter.deprecated :
Lean.Option Bool
source
structure Lean.Linter.DeprecationEntry :
Type
Instances For
    source
    instance Lean.Linter.instInhabitedDeprecationEntry :
    Inhabited Lean.Linter.DeprecationEntry
    source
    opaque Lean.Linter.deprecatedAttr :
    Lean.ParametricAttribute Lean.Linter.DeprecationEntry
    source
    def Lean.Linter.isDeprecated (env : Lean.Environment) (declName : Lean.Name) :
    Bool
    Instances For
      source
      def Lean.MessageData.isDeprecationWarning (msg : Lean.MessageData) :
      Bool
      Instances For
        source
        def Lean.Linter.getDeprecatedNewName (env : Lean.Environment) (declName : Lean.Name) :
        Option Lean.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 : Lean.Name) :
          m Unit
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For