structure Lean.ParseImports.State : Type

• imports : Array Lean.Import
• pos : String.Pos
• error? : Option String

instance Lean.ParseImports.instInhabitedState : Inhabited Lean.ParseImports.State

Equations

• Lean.ParseImports.instInhabitedState = { default := { imports := default, pos := default, error? := default } }

def Lean.ParseImports.Parser : Type

Equations

• Lean.ParseImports.Parser = (String → Lean.ParseImports.State → Lean.ParseImports.State)

instance Lean.ParseImports.instInhabitedParser : Inhabited Lean.ParseImports.Parser

Equations

• Lean.ParseImports.instInhabitedParser = { default := fun (x : String) (s : Lean.ParseImports.State) => s }

@[inline]

def Lean.ParseImports.State.setPos (s : Lean.ParseImports.State) (pos : String.Pos) : Lean.ParseImports.State

Equations

• s.setPos pos = { imports := s.imports, pos := pos, error? := s.error? }

@[inline]

def Lean.ParseImports.State.mkError (s : Lean.ParseImports.State) (msg : String) : Lean.ParseImports.State

Equations

• s.mkError msg = { imports := s.imports, pos := s.pos, error? := some msg }

def Lean.ParseImports.State.mkEOIError (s : Lean.ParseImports.State) : Lean.ParseImports.State

Equations

• s.mkEOIError = s.mkError "unexpected end of input"

@[inline]

def Lean.ParseImports.State.next (s : Lean.ParseImports.State) (input : String) (pos : String.Pos) : Lean.ParseImports.State

Equations

• s.next input pos = { imports := s.imports, pos := input.next pos, error? := s.error? }

@[inline]

def Lean.ParseImports.State.next' (s : Lean.ParseImports.State) (input : String) (pos : String.Pos) (h : ¬input.atEnd pos = true) : Lean.ParseImports.State

Equations

• s.next' input pos h = { imports := s.imports, pos := input.next' pos h, error? := s.error? }

partial def Lean.ParseImports.finishCommentBlock (nesting : Nat) : Lean.ParseImports.Parser

def Lean.ParseImports.finishCommentBlock.eoi (s : Lean.ParseImports.State) : Lean.ParseImports.State

Equations

• Lean.ParseImports.finishCommentBlock.eoi s = s.mkError "unterminated comment"

@[specialize #[]]

partial def Lean.ParseImports.takeUntil (p : Char → Bool) : Lean.ParseImports.Parser

@[inline]

def Lean.ParseImports.takeWhile (p : Char → Bool) : Lean.ParseImports.Parser

Equations

• Lean.ParseImports.takeWhile p = Lean.ParseImports.takeUntil fun (c : Char) => !p c

@[inline]

def Lean.ParseImports.andthen (p : Lean.ParseImports.Parser) (q : Lean.ParseImports.Parser) : Lean.ParseImports.Parser

Equations

• Lean.ParseImports.andthen p q input s = let s := p input s; if (match s.error? with | some val => true | x => false) = true then s else q input s

instance Lean.ParseImports.instAndThenParser : AndThen Lean.ParseImports.Parser

Equations

• Lean.ParseImports.instAndThenParser = { andThen := fun (p : Lean.ParseImports.Parser) (q : Unit → Lean.ParseImports.Parser) => Lean.ParseImports.andthen p (q ()) }

partial def Lean.ParseImports.whitespace : Lean.ParseImports.Parser

@[inline]

def Lean.ParseImports.keywordCore (k : String) (failure : Lean.ParseImports.Parser) (success : Lean.ParseImports.Parser) : Lean.ParseImports.Parser

Equations

• Lean.ParseImports.keywordCore k failure success input s = Lean.ParseImports.keywordCore.go k failure success input s 0 s.pos

@[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) : Lean.ParseImports.State

@[inline]

def Lean.ParseImports.keyword (k : String) : Lean.ParseImports.Parser

Equations

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

@[inline]

def Lean.ParseImports.isIdCont : String → Lean.ParseImports.State → Bool

Equations

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

def Lean.ParseImports.State.pushModule (module : Lake.Name) (runtimeOnly : Bool) (s : Lean.ParseImports.State) : Lean.ParseImports.State

Equations

• Lean.ParseImports.State.pushModule module runtimeOnly s = { imports := s.imports.push { module := module, runtimeOnly := runtimeOnly }, pos := s.pos, error? := s.error? }

@[inline]

def Lean.ParseImports.isIdRestCold (c : Char) : Bool

Equations

• Lean.ParseImports.isIdRestCold c = (decide (c = '_') || decide (c = ''') || c == '!' || c == '?' || Lean.isLetterLike c || Lean.isSubScriptAlnum c)

@[inline]

def Lean.ParseImports.isIdRestFast (c : Char) : Bool

Equations

• Lean.ParseImports.isIdRestFast c = (c.isAlphanum || c != '.' && c != '\n' && c != ' ' && Lean.ParseImports.isIdRestCold c)

def Lean.ParseImports.moduleIdent (runtimeOnly : Bool) : Lean.ParseImports.Parser

Equations

• Lean.ParseImports.moduleIdent runtimeOnly input s = Lean.ParseImports.moduleIdent.parse runtimeOnly input Lean.Name.anonymous s

partial def Lean.ParseImports.moduleIdent.parse (runtimeOnly : Bool) (input : String) (module : Lake.Name) (s : Lean.ParseImports.State) : Lean.ParseImports.State

@[specialize #[]]

partial def Lean.ParseImports.many (p : Lean.ParseImports.Parser) : Lean.ParseImports.Parser

@[inline]

def Lean.ParseImports.preludeOpt (k : String) : Lean.ParseImports.Parser

Equations

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

def Lean.ParseImports.main : Lean.ParseImports.Parser

Equations

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

def Lean.parseImports' (input : String) (fileName : String) : IO (Array Lean.Import)

Simpler and faster version of parseImports. We use it to implement Lake.

Equations

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

instance Lean.instToJsonImport : Lean.ToJson Lean.Import

Equations

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

structure Lean.PrintImportResult : Type

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

instance Lean.instToJsonPrintImportResult : Lean.ToJson Lean.PrintImportResult

Equations

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

structure Lean.PrintImportsResult : Type

• imports : Array Lean.PrintImportResult

instance Lean.instToJsonPrintImportsResult : Lean.ToJson Lean.PrintImportsResult

Equations

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

@[export lean_print_imports_json]

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

Equations

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