def Lean.Elab.headerToImports (header : Lean.Syntax) : List 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) : 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 (List 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.

instance Lean.Elab.instToJsonImport : Lean.ToJson Lean.Import

Equations

• Lean.Elab.instToJsonImport = { toJson := Lean.Elab.toJsonImport✝ }

structure Lean.Elab.PrintImportResult : Type

• imports? : Option (Array Lean.Import)
• errors : Array String

instance Lean.Elab.instToJsonPrintImportResult : Lean.ToJson Lean.Elab.PrintImportResult

Equations

• Lean.Elab.instToJsonPrintImportResult = { toJson := Lean.Elab.toJsonPrintImportResult✝ }

structure Lean.Elab.PrintImportsResult : Type

• imports : Array Lean.Elab.PrintImportResult

instance Lean.Elab.instToJsonPrintImportsResult : Lean.ToJson Lean.Elab.PrintImportsResult

Equations

• Lean.Elab.instToJsonPrintImportsResult = { toJson := Lean.Elab.toJsonPrintImportsResult✝ }

@[export lean_print_imports_json]

def Lean.Elab.printImportsJson (fileNames : Array String) : IO Unit

Equations

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