def Lean.Parser.Module.prelude : Lean.Parser.Parser

Equations

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

def Lean.Parser.Module.import : Lean.Parser.Parser

Equations

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

def Lean.Parser.Module.header : Lean.Parser.Parser

Equations

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

def Lean.Parser.Module.module : Lean.Parser.Parser

Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that return the same syntax tree structure, but add error recovery. Still, it is helpful to have a Parser definition for it in order to auto-generate helpers such as the pretty printer.

Equations

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

def Lean.Parser.Module.updateTokens (tokens : Lean.Parser.TokenTable) : Lean.Parser.TokenTable

Equations

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

structure Lean.Parser.ModuleParserState : Type

• pos : String.Pos
• recovering : Bool

instance Lean.Parser.instInhabitedModuleParserState : Inhabited Lean.Parser.ModuleParserState

Equations

• Lean.Parser.instInhabitedModuleParserState = { default := { pos := default, recovering := default } }

def Lean.Parser.parseHeader (inputCtx : Lean.Parser.InputContext) : IO (Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog)

Equations

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

def Lean.Parser.isEOI (s : Lean.Syntax) : Bool

Equations

• Lean.Parser.isEOI s = Lean.Syntax.isOfKind s `Lean.Parser.Module.eoi

def Lean.Parser.isTerminalCommand (s : Lean.Syntax) : Bool

Equations

• Lean.Parser.isTerminalCommand s = (Lean.Syntax.isOfKind s `Lean.Parser.Command.exit || Lean.Syntax.isOfKind s `Lean.Parser.Command.import)

def Lean.Parser.topLevelCommandParserFn : Lean.Parser.ParserFn

Equations

• Lean.Parser.topLevelCommandParserFn = Lean.Parser.commandParser.fn

def Lean.Parser.parseCommand (inputCtx : Lean.Parser.InputContext) (pmctx : Lean.Parser.ParserModuleContext) (mps : Lean.Parser.ModuleParserState) (messages : Lean.MessageLog) : Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog

Equations

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

def Lean.Parser.testParseModuleAux (env : Lean.Environment) (inputCtx : Lean.Parser.InputContext) (s : Lean.Parser.ModuleParserState) (msgs : Lean.MessageLog) (stxs : Array Lean.Syntax) : IO (Array Lean.Syntax)

Equations

• Lean.Parser.testParseModuleAux env inputCtx s msgs stxs = Lean.Parser.testParseModuleAux.parse env inputCtx s msgs stxs

partial def Lean.Parser.testParseModuleAux.parse (env : Lean.Environment) (inputCtx : Lean.Parser.InputContext) (state : Lean.Parser.ModuleParserState) (msgs : Lean.MessageLog) (stxs : Array Lean.Syntax) : IO (Array Lean.Syntax)

def Lean.Parser.testParseModule (env : Lean.Environment) (fname : String) (contents : String) : IO (Lean.TSyntax `Lean.Parser.Module.module)

Equations

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

def Lean.Parser.testParseFile (env : Lean.Environment) (fname : System.FilePath) : IO (Lean.TSyntax `Lean.Parser.Module.module)

Equations

• Lean.Parser.testParseFile env fname = do let contents ← IO.FS.readFile fname Lean.Parser.testParseModule env fname.toString contents