Documentation

Lean.Linter.Deprecated

Instances For
    def Lean.Linter.setDeprecated {m : TypeType} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (entry : DeprecationEntry) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def Lean.Linter.isDeprecated (env : Environment) (declName : Name) :
      Equations
      Instances For
        Equations
        Instances For
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For