opaque Lean.Linter.linter.coreInternal.internalModule : Lean.Option Bool

Enables the Lean core internalModule linter, which warns when a module considered "internal" declares a declaration that is not itself "internal".

The intent is that declarations living in internal modules (for example, anything under the Lean namespace, or the omega/grind implementation modules) stay internal, rather than becoming part of a project's public API by accident.

This linter is off by default and is not intended for use by non-core projects. It is a member of the linter.coreInternal set, so it can also be enabled via set_option linter.coreInternal true.

def Lean.Linter.InternalModule.internalNameComponents : Array String

A module or declaration is internal if one of its name components is one of these strings.

def Lean.Linter.InternalModule.hasInternalNameComponent : Name → Bool

Whether one of the components of n is in internalNameComponents.

def Lean.Linter.InternalModule.internalModulePrefixes : Array Name

A module is internal if it is (a submodule of) one of these modules.

def Lean.Linter.InternalModule.isInternalModule (mod : Name) : Bool

Whether mod is an "internal" module, i.e. one whose declarations should stay internal.

def Lean.Linter.InternalModule.internalDeclNamespaces : Array Name

A declaration is internal if it lives in (a namespace under) one of these namespaces.

def Lean.Linter.InternalModule.isInternalDecl (declName : Name) : Bool

Whether declName is an "internal" declaration.

def Lean.Linter.InternalModule.internalModuleLinter : Linter

Enables the Lean core internalModule linter, which warns when a module considered "internal" declares a declaration that is not itself "internal".

The intent is that declarations living in internal modules (for example, anything under the Lean namespace, or the omega/grind implementation modules) stay internal, rather than becoming part of a project's public API by accident.

This linter is off by default and is not intended for use by non-core projects. It is a member of the linter.coreInternal set, so it can also be enabled via set_option linter.coreInternal true.