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

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.processHeaderCore (startPos : String.Pos) (imports : Array Import) (isModule : Bool) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv : Bool := false) (mainModule : Name := Name.anonymous) (arts : NameMap ImportArtifacts := ∅) : 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 System.FilePath := #[]) (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.