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

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

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

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.

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

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

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