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

Equations

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

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

Equations

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

def Lean.Elab.parseImports (input : String) (fileName : optParam (Option String) none) : IO (Array Lean.Import × Lean.Position × Lean.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.