def Lean.Parser.Module.moduleTk : Parser

def Lean.Parser.Module.prelude : Parser

def Lean.Parser.Module.public : Parser

def Lean.Parser.Module.meta : Parser

def Lean.Parser.Module.all : Parser

def Lean.Parser.Module.import : Parser

def Lean.Parser.Module.header : Parser

def Lean.Parser.Module.module : 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 : TokenTable) : TokenTable

structure Lean.Parser.ModuleParserState : Type

• pos : String.Pos
• recovering : Bool

instance Lean.Parser.instInhabitedModuleParserState : Inhabited ModuleParserState

def Lean.Parser.parseHeader (inputCtx : InputContext) : IO (TSyntax `Lean.Parser.Module.header × ModuleParserState × MessageLog)

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

def Lean.Parser.topLevelCommandParserFn : ParserFn

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

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

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

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

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