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.

Equations

• Lean.Linter.InternalModule.internalNameComponents = #["Internal"]

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

Whether one of the components of n is in internalNameComponents.

Equations

• Lean.Linter.InternalModule.hasInternalNameComponent (p.str s) = (Lean.Linter.InternalModule.internalNameComponents.contains s || Lean.Linter.InternalModule.hasInternalNameComponent p)
• Lean.Linter.InternalModule.hasInternalNameComponent (p.num i) = Lean.Linter.InternalModule.hasInternalNameComponent p
• Lean.Linter.InternalModule.hasInternalNameComponent Lean.Name.anonymous = false

def Lean.Linter.InternalModule.internalModulePrefixes : Array Name

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

Equations

• Lean.Linter.InternalModule.internalModulePrefixes = #[`Init.Omega, `Init.Grind, `Lean, `Lake, `IMLinterTest]

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

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

Equations

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

def Lean.Linter.InternalModule.internalDeclNamespaces : Array Name

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

Equations

• Lean.Linter.InternalModule.internalDeclNamespaces = #[`Lean, `Lake]

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

Whether declName is an "internal" declaration.

Equations

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

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.

Equations

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