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
Instances For
def
Lean.Parser.parseHeader
(inputCtx : InputContext)
:
IO (TSyntax `Lean.Parser.Module.header × ModuleParserState × MessageLog)
Equations
Instances For
def
Lean.Parser.parseCommand
(inputCtx : InputContext)
(pmctx : ParserModuleContext)
(mps : ModuleParserState)
(messages : MessageLog)
:
Equations
Instances For
def
Lean.Parser.testParseModuleAux
(env : Environment)
(inputCtx : InputContext)
(s : ModuleParserState)
(msgs : MessageLog)
(stxs : Array Syntax)
:
Equations
Instances For
partial def
Lean.Parser.testParseModuleAux.parse
(env : Environment)
(inputCtx : InputContext)
(state : ModuleParserState)
(msgs : MessageLog)
(stxs : Array Syntax)
: