@[reducible, inline]

abbrev Lean.Elab.HeaderSyntax : Type

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

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

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

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

@[reducible, inline]

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

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.

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

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)

@[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.

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

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

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