Documentation
Lean
.
Elab
.
Import
Search
Google site search
Lean
.
Elab
.
Import
source
Imports
Init
Lean.Data.Json
Lean.Parser.Module
Imported by
Lean
.
Elab
.
headerToImports
Lean
.
Elab
.
processHeader
Lean
.
Elab
.
parseImports
Lean
.
Elab
.
printImports
source
def
Lean
.
Elab
.
headerToImports
(header :
Lean.Syntax
)
:
Array
Lean.Import
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
)
Instances For
source
def
Lean
.
Elab
.
parseImports
(input :
String
)
(fileName :
optParam
(
Option
String
)
none
)
:
IO
(
Array
Lean.Import
×
Lean.Position
×
Lean.MessageLog
)
Instances For
source
@[export lean_print_imports]
def
Lean
.
Elab
.
printImports
(input :
String
)
(fileName :
Option
String
)
:
IO
Unit
Instances For