Documentation

Lean.Elab.Import

source
def Lean.Elab.headerToImports (header : Lean.Syntax) :
Array Lean.Import
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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.
    Instances For
      source
      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.
      Instances For
        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.
        Instances For