# The `upstreamableDecl` linter #

The `upstreamableDecl` linter detects declarations that could be moved to a file higher up in the import hierarchy. This is intended to assist with splitting files.

source
def Lean.Name.isLocal (env : Environment) (decl : Name) :
Bool

Does this declaration come from the current file?

Equations

- Lean.Name.isLocal env decl = (env.getModuleIdxFor? decl).isNone

Instances For

source
def Lean.Environment.localDefinitionDependencies (env : Environment) (stx id : Syntax) :
Elab.Command.CommandElabM Bool

Does the declaration with this name depend on definitions in the current file?

Here, "definition" means everything that is not a theorem, and so includes `def`, `structure`, `inductive`, etc.

Equations

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

Instances For

source
opaque Mathlib.Linter.linter.upstreamableDecl :
Lean.Option Bool

The `upstreamableDecl` linter detects declarations that could be moved to a file higher up in the import hierarchy. If this is the case, it emits a warning.

By default, this linter will not fire on definitions, nor private declarations: see options `linter.upstreamableDecl.defs` and `linter.upstreamableDecl.private`.

This is intended to assist with splitting files.

source
opaque Mathlib.Linter.linter.upstreamableDecl.defs :
Lean.Option Bool

If set to `true`, the `upstreamableDecl` linter will add warnings on definitions.

The linter does not place a warning on any declaration depending on a definition in the current file (while it does place a warning on the definition itself), since we often create a new file for a definition on purpose.

source
opaque Mathlib.Linter.linter.upstreamableDecl.private :
Lean.Option Bool

If set to `true`, the `upstreamableDecl` linter will add warnings on private declarations.

source
def Mathlib.Linter.DoubleImports.upstreamableDeclLinter :
Lean.Linter

The `upstreamableDecl` linter detects declarations that could be moved to a file higher up in the import hierarchy. If this is the case, it emits a warning.

By default, this linter will not fire on definitions, nor private declarations: see options `linter.upstreamableDecl.defs` and `linter.upstreamableDecl.private`.

This is intended to assist with splitting files.

Equations

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

Instances For