@[reducible, inline]
Equations
Instances For
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 ModuleArtifacts := ∅)
:
Equations
Instances For
@[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)
:
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.