Documentation

Lean.Elab.Import

source
def Lean.Elab.headerToImports (header : Syntax) :
Array Import
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.processHeader (header : Syntax) (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext) (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv : Bool := false) :
IO (Environment × MessageLog)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
@[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.
source
@[export lean_print_import_srcs]
def Lean.Elab.printImportSrcs (input : String) (fileName : Option String) :
IO Unit
Equations
  • One or more equations did not get rendered due to their size.