@[reducible, inline]

abbrev Lean.Elab.HeaderSyntax : Type

Equations

• Lean.Elab.HeaderSyntax = Lean.TSyntax `Lean.Parser.Module.header

def Lean.Elab.HeaderSyntax.startPos (header : HeaderSyntax) : String.Pos.Raw

Equations

• header.startPos = header.raw.getPos?.getD 0

def Lean.Elab.HeaderSyntax.isModule (header : HeaderSyntax) : Bool

Equations

• header.isModule = !header.raw[0].isNone

def Lean.Elab.HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import

Equations

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

def Lean.Elab.HeaderSyntax.toModuleHeader (stx : HeaderSyntax) : ModuleHeader

Equations

• stx.toModuleHeader = { imports := stx.imports, isModule := stx.isModule }

@[reducible, inline]

abbrev Lean.Elab.headerToImports (stx : HeaderSyntax) (includeInit : Bool := true) : Array Import

Equations

• @Lean.Elab.headerToImports = @Lean.Elab.HeaderSyntax.imports

def Lean.Elab.checkDeprecatedImports (env : Environment) (imports : Array Import) (opts : Options) (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw) (messages : MessageLog) (headerStx? origHeaderStx? : Option HeaderSyntax := none) : MessageLog

Check imported modules for deprecation and emit warnings.

The -- deprecated_module: ignore comment can be placed on the module keyword to suppress all warnings, or on individual import statements to suppress specific ones. This follows the same pattern as -- shake: keep in Lake shake.

The headerStx? parameter carries the header syntax used for checking trailing comments. When called from the Language Server, the main header syntax may have its trailing trivia stripped by unsetTrailing for caching purposes, so origHeaderStx? can supply the original (untrimmed) syntax to preserve -- deprecated_module: ignore annotations on the last import.

Equations

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

def Lean.Elab.checkModuleNamePortability (mainModule : Name) (inputCtx : Parser.InputContext) (startPos : String.Pos.Raw) (messages : MessageLog) : MessageLog

Equations

• Lean.Elab.checkModuleNamePortability mainModule inputCtx startPos messages = Lean.Elab.checkModuleNamePortability.go✝ mainModule inputCtx startPos mainModule messages

def Lean.Elab.processHeaderCore (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (plugins : Array Plugin := #[]) (leakEnv : Bool := false) (mainModule : Name := Name.anonymous) (package? : Option PkgId := none) (arts : NameMap ImportArtifacts := ∅) (headerStx? origHeaderStx? : Option HeaderSyntax := none) : IO (Environment × MessageLog)

Equations

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

@[inline]

def Lean.Elab.processHeader (header : HeaderSyntax) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (plugins : Array Plugin := #[]) (leakEnv : Bool := false) (mainModule : Name := Name.anonymous) : IO (Environment × MessageLog)

Elaborates the given header syntax into an environment.

If mainModule is not given, Environment.setMainModule should be called manually. This is a backwards compatibility measure not compatible with the module system.

Equations

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

def Lean.Elab.parseImports (input : String) (fileName : Option String := none) : IO (Array Import × Position × MessageLog)

Equations

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

def Lean.Elab.printImports (input : String) (fileName : Option String) : IO Unit

Equations

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

def Lean.Elab.printImportSrcs (input : String) (fileName : Option String) : IO Unit

Equations

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