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 DeprecationEntry
    Equations
      source
      opaque Lean.Linter.deprecatedAttr :
      ParametricAttribute DeprecationEntry
      source
      def Lean.Linter.isDeprecated (env : Environment) (declName : Name) :
      Bool
      Equations
        Instances For
          source
          def Lean.MessageData.isDeprecationWarning (msg : MessageData) :
          Bool
          Equations
            Instances For
              source
              def Lean.Linter.getDeprecatedNewName (env : Environment) (declName : Name) :
              Option Name
              Equations
                Instances For
                  source
                  def Lean.Linter.checkDeprecated {m : Type → Type} [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) :
                  m Unit
                  Equations
                    Instances For