def Lean.Elab.headerToImports (header : Syntax) : Array Import

Equations

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

def Lean.Elab.processHeader (header : Syntax) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (leakEnv : Bool := false) : IO (Environment × MessageLog)

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.

@[export lean_print_imports]

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

Equations

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