- imports : Array Lean.Import
- pos : String.Pos
Instances For
@[inline]
Instances For
@[inline]
Instances For
Instances For
@[inline]
def
Lean.ParseImports.State.next
(s : Lean.ParseImports.State)
(input : String)
(pos : String.Pos)
:
Instances For
@[inline]
def
Lean.ParseImports.State.next'
(s : Lean.ParseImports.State)
(input : String)
(pos : String.Pos)
(h : ¬String.atEnd input pos = true)
:
Instances For
Instances For
@[specialize #[]]
@[inline]
Instances For
@[inline]
Instances For
@[inline]
def
Lean.ParseImports.keywordCore
(k : String)
(failure : Lean.ParseImports.Parser)
(success : Lean.ParseImports.Parser)
:
Instances For
@[specialize #[]]
partial def
Lean.ParseImports.keywordCore.go
(k : String)
(failure : Lean.ParseImports.Parser)
(success : Lean.ParseImports.Parser)
(input : String)
(s : Lean.ParseImports.State)
(i : String.Pos)
(j : String.Pos)
:
@[inline]
Instances For
def
Lean.ParseImports.State.pushModule
(module : Lake.Name)
(runtimeOnly : Bool)
(s : Lean.ParseImports.State)
:
Instances For
partial def
Lean.ParseImports.moduleIdent.parse
(runtimeOnly : Bool)
(input : String)
(module : Lake.Name)
(s : Lean.ParseImports.State)
:
@[specialize #[]]
@[inline]
Instances For
Simpler and faster version of parseImports
. We use it to implement Lake.
Instances For
- imports? : Option (Array Lean.Import)