ImportLinter.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 0 contain sorry, 0 declared as axioms

The Import Linter

This file implements a linter that enforces import conventions in FormalConjectures:

Disallow direct Mathlib and FormalConjecturesForMathlib imports: Problem files in FormalConjectures must not import Mathlib, Mathlib.*, FormalConjecturesForMathlib, or any FormalConjecturesForMathlib.* module directly. They should use import FormalConjecturesUtil instead.
Require FormalConjecturesUtil: Problem files in FormalConjectures must import FormalConjecturesUtil.
Keep meta imports narrow: A meta import does not bring any declarations into scope; it only loads the compiled code of the imported module (and of its transitive imports), which is what native_decide and #eval need under the module system. meta imports are therefore exempt from the first rule, but they must name the module defining the evaluated declaration: meta import FormalConjecturesUtil, meta import FormalConjecturesForMathlib and meta import Mathlib load the compiled code of the whole library and are disallowed.
Require modules: Problem files in FormalConjectures must be modules, and they must import FormalConjecturesUtil with public import. In a module, a plain import is private, so the statements of public declarations cannot use it.

Imports (2)

Imported by 2 files

structure ImportLinter.ImportRef An import of a parsed header, retaining its syntax node line 62 source
Source documentation
An import of a parsed header, retaining its syntax node.
TODO(v4.34.0): Replace ImportRef, ImportRef.getIdent, and headerToImportRefs with ImportGraph.Lean.headerToImportRefs from ImportGraph.Imports.Pretty (added in leanprover-community/import-graph#133).

no axioms what this means
```
structure ImportRef extends Import where
…
```
def ImportLinter.ImportRef.getIdent Extracts the module identifier from an ImportRef line 68 source
Source documentation
Extracts the module identifier from an ImportRef.

standard axioms: propext what this means
Statement uses: ImportLinter.ImportRef, Lean.Syntax.Ident
Proof uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr4, List.nil, ImportLinter.ImportRef.stx, ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Unit, cond, Bool.or, Bool.false and 7 more
2 instances, coercions and auxiliary constants left out.
```
def ImportRef.getIdent (i : ImportRef) : Ident :=
…
```
Mentions: ImportLinter.ImportRef
def ImportLinter.headerToImportRefs Collects every import of a parsed header, with its modifiers and syntax line 74 source
Source documentation
Collects every import of a parsed header, with its modifiers and syntax.

standard axioms: propext what this means
Statement uses: Lean.TSyntax, List.cons, Lean.SyntaxNodeKind, Lean.Name.mkStr4, List.nil, Array, ImportLinter.ImportRef
Proof uses: ite, Eq, Bool, Lean.Syntax.isOfKind, Lean.TSyntax.raw, Bool.true, Lean.Syntax, Lean.Syntax.getArg, OfNat.ofNat, Nat, Unit, Option, Lean.TSyntaxArray, Lean.TSyntaxArray.mk, Lean.Syntax.getArgs, Array.map, cond, Bool.or, Bool.false, Lean.Name.mkStr1 and 14 more
2 instances, coercions and auxiliary constants left out.
```
def headerToImportRefs (header : TSyntax ``Parser.Module.header) : Array ImportRef :=
…
```
Mentions: ImportLinter.ImportRef
def ImportLinter.checkImports Checks a parsed header against the Formal Conjectures import rules line 92 source
Source documentation
Checks a parsed header against the Formal Conjectures import rules. meta imports are exempt from the rules on direct Mathlib and FormalConjecturesForMathlib imports.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.Elab.HeaderSyntax, optParam, Bool, Bool.true, Lean.Syntax, Lean.Syntax.missing, Lean.Elab.Command.CommandElabM, Unit
Proof uses: Array, ImportLinter.ImportRef, ImportLinter.headerToImportRefs, Bind.bind, PUnit, ForIn.forIn, inferInstance, Membership, PUnit.unit, Lean.Name, Lean.Import.module, ImportLinter.ImportRef.toImport, ite, ForInStep, Eq, Lean.Import.isMeta, Pure.pure, Lean.Elab.Command.Context, StateRefT', IO.RealWorld and 40 more
27 instances, coercions and auxiliary constants left out.
```
def checkImports (header : HeaderSyntax) (isFormalConjecturesModule : Bool := true)
…
```
def ImportLinter.importLinter The import linter ensures that: - Files in FormalConjectures do not import Mathlib, Mathlib.*, FormalConjecturesForMathlib, or FormalConjecturesForMathlib.* directly line 140 source
Source documentation
The import linter ensures that:
- Files in FormalConjectures do not import Mathlib, Mathlib.*, FormalConjecturesForMathlib, or FormalConjecturesForMathlib.* directly.
- Files in FormalConjectures import FormalConjecturesUtil.
- Files in FormalConjectures do not meta import a whole library (FormalConjecturesUtil, FormalConjecturesForMathlib or Mathlib).
- Files in FormalConjectures are modules that public import FormalConjecturesUtil.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Lean.Elab.Command.Linter
Proof uses: Lean.Elab.Command.Linter.mk, Lean.withSetOptionIn, Lean.Syntax, ite, Lean.Elab.Command.CommandElabM, Unit, Eq, Bool, BEq.beq, Lean.SyntaxNodeKind, Lean.Syntax.getKind, Lean.Name.mkStr4, Bool.true, Pure.pure, Lean.Elab.Command.Context, StateRefT', IO.RealWorld, Lean.Elab.Command.State, EIO, Lean.Exception and 41 more
29 instances, coercions and auxiliary constants left out.
```
def importLinter : Linter where run := withSetOptionIn fun stx ↦ do
…
```