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?

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.

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.

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.