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.

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

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.

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.

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

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