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 : Lean.Environment) (decl : Lean.Name) : Bool

Does this declaration come from the current file?

Equations

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

def Lean.Environment.localDefinitionDependencies (env : Lean.Environment) (stx id : Lean.Syntax) : Lean.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.

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.

This is intended to assist with splitting files.

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.

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.

This is intended to assist with splitting files.

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.

Equations

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