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

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

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

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

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

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)

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 contents : String) : IO (Lean.TSyntax `Lean.Parser.Module.module)

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