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

Equations

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

structure Lean.Parser.ModuleParserState : Type

• pos : String.Pos.Raw
• recovering : Bool
• hasLeading : Bool

  Whether there is leading whitespace before pos. Used to associate whitespace at the start of the file with the first token of the file.

@[instance_reducible]

instance Lean.Parser.instInhabitedModuleParserState : Inhabited ModuleParserState

Equations

• Lean.Parser.instInhabitedModuleParserState = { default := Lean.Parser.instInhabitedModuleParserState.default }

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

Equations

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

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

Equations

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

def Lean.Parser.topLevelCommandParserFn : ParserFn

Equations

• Lean.Parser.topLevelCommandParserFn = (Lean.Parser.withPosition Lean.Parser.commandParser).fn

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

Equations

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

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

Equations

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

def Lean.Parser.testParseModule (env : Environment) (fname contents : String) : IO Syntax

Equations

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

def Lean.Parser.testParseFile (env : Environment) (fname : System.FilePath) : IO Syntax

Equations

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