@[reducible, inline]

abbrev Lean.Parser.mkAtom (info : SourceInfo) (val : String) : Syntax

Equations

• Lean.Parser.mkAtom info val = Lean.Syntax.atom info val

@[reducible, inline]

abbrev Lean.Parser.mkIdent (info : SourceInfo) (rawVal : Substring) (val : Name) : Syntax

Equations

• Lean.Parser.mkIdent info rawVal val = Lean.Syntax.ident info rawVal val []

def Lean.Parser.getNext (input : String) (pos : String.Pos) : Char

Return character after position pos

Equations

• Lean.Parser.getNext input pos = input.get (input.next pos)

def Lean.Parser.maxPrec : Nat

Maximal (and function application) precedence. In the standard lean language, no parser has precedence higher than maxPrec.

Note that nothing prevents users from using a higher precedence, but we strongly discourage them from doing it.

Equations

• Lean.Parser.maxPrec = 1024

def Lean.Parser.argPrec : Nat

Equations

• Lean.Parser.argPrec = 1023

def Lean.Parser.leadPrec : Nat

Equations

• Lean.Parser.leadPrec = 1022

def Lean.Parser.minPrec : Nat

Equations

• Lean.Parser.minPrec = 10

@[reducible, inline]

abbrev Lean.Parser.Token : Type

Equations

• Lean.Parser.Token = String

@[reducible, inline]

abbrev Lean.Parser.TokenTable : Type

Equations

• Lean.Parser.TokenTable = Lean.Data.Trie Lean.Parser.Token

@[reducible, inline]

abbrev Lean.Parser.SyntaxNodeKindSet : Type

Equations

• Lean.Parser.SyntaxNodeKindSet = Lean.PersistentHashMap Lean.SyntaxNodeKind Unit

def Lean.Parser.SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet

Equations

• s.insert k = Lean.PersistentHashMap.insert s k ()

structure Lean.Parser.InputContext : Type

Input string and related data. Recall that the FileMap is a helper structure for mapping String.Pos in the input string to line/column information.

• mk' :: (
• inputString : String
• fileName : String
• fileMap : FileMap
• endPos : String.Pos
• endPos_valid : self.endPos ≤ self.inputString.endPos
• )

instance Lean.Parser.instInhabitedInputContext : Inhabited InputContext

Equations

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

def Lean.Parser.InputContext.mk (input fileName : String) (endPos : String.Pos := input.endPos) (endPos_valid : endPos ≤ input.endPos := by simp) (fileMap : FileMap := FileMap.ofString input) : InputContext

Equations

• Lean.Parser.InputContext.mk input fileName endPos endPos_valid fileMap = { inputString := input, fileName := fileName, fileMap := fileMap, endPos := endPos, endPos_valid := endPos_valid }

@[deprecated "Call `InputContext.get`, `InputContext.get'`, `InputContext.next'`, and `InputContext.atEnd` directly" (since := "2025-08-21")]

def Lean.Parser.InputContext.input (c : InputContext) : String

Equations

• c.input = c.inputString.extract 0 c.endPos

def Lean.Parser.InputContext.atEnd (c : InputContext) (p : String.Pos) : Bool

Returns true if a specified byte position is greater than or equal to the position which points to the end of the input string. Otherwise, returns false.

Equations

• c.atEnd p = decide (p ≥ c.endPos)

@[inline]

def Lean.Parser.InputContext.get (c : InputContext) (p : String.Pos) : Char

Returns the character at position p of the input string. If p is not a valid position, returns the fallback value (default : Char), which is 'A', but does not panic.

Equations

• c.get p = c.inputString.get p

theorem Lean.Parser.InputContext.not_atEnd_inputString {c : InputContext} {p : String.Pos} : ¬c.atEnd p = true → ¬c.inputString.atEnd p = true

@[inline]

def Lean.Parser.InputContext.get' (c : InputContext) (p : String.Pos) (h : ¬c.atEnd p = true) : Char

Returns the character at position p of the input string. Returns (default : Char), which is 'A', if p is not a valid position.

Requires evidence, h, that p is within bounds instead of performing a run-time bounds check as in InputContext.get.

A typical pattern combines get' with a dependent if-expression to avoid the overhead of an additional bounds check. For example:

def getInBounds? (s : String) (p : String.Pos) : Option Char :=
  if h : s.atEnd p then none else some (s.get' p h)

Even with evidence of ¬ s.atEnd p, p may be invalid if a byte index points into the middle of a multi-byte UTF-8 character.

Equations

• c.get' p h = c.inputString.get' p ⋯

@[inline]

def Lean.Parser.InputContext.next (c : InputContext) (p : String.Pos) : String.Pos

Returns the next position in the input string after position p. If p is not a valid position or p = c.endPos, returns the position one byte after p.

A run-time bounds check is performed to determine whether p is at the end of the string. If a bounds check has already been performed, use InputContext.next' to avoid a repeated check.

Equations

• c.next p = c.inputString.next p

@[inline]

def Lean.Parser.InputContext.next' (c : InputContext) (p : String.Pos) (h : ¬c.atEnd p = true) : String.Pos

Returns the next position in the input string after position p. The result is unspecified if p is not a valid position.

Requires evidence, h, that p is within bounds. No run-time bounds check is performed.

Equations

• c.next' p h = c.inputString.next' p ⋯

@[inline]

def Lean.Parser.InputContext.extract (c : InputContext) : String.Pos → String.Pos → String

Creates a new string that consists of the region of the input string delimited by the two positions.

The result is "" if the start position is greater than or equal to the end position or if the start position is at the end of the string. If either position is invalid (that is, if either points at the middle of a multi-byte UTF-8 character) then the result is unspecified.

Equations

• c.extract = c.inputString.extract

@[inline]

def Lean.Parser.InputContext.substring (c : InputContext) (startPos stopPos : String.Pos) : Substring

Extracts a substring of the input string, bounded by startPos and stopPos.

Equations

• c.substring startPos stopPos = { str := c.inputString, startPos := startPos, stopPos := min stopPos c.endPos }

@[inline]

def Lean.Parser.InputContext.getNext (input : InputContext) (pos : String.Pos) : Char

Return character after position pos

Equations

• input.getNext pos = input.get (input.next pos)

@[inline]

def Lean.Parser.InputContext.prev (c : InputContext) (pos : String.Pos) : String.Pos

Returns the character position prior to pos

Equations

• c.prev pos = c.inputString.prev pos

structure Lean.Parser.ParserModuleContext : Type

Input context derived from elaboration of previous commands.

• env : Environment
• options : Options
• currNamespace : Name
• openDecls : List OpenDecl

structure Lean.Parser.CacheableParserContext : Type

Parser context parts that can be updated without invalidating the parser cache.

• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token

def Lean.Parser.instBEqCacheableParserContext.beq : CacheableParserContext → CacheableParserContext → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.instBEqCacheableParserContext.beq x✝¹ x✝ = false

instance Lean.Parser.instBEqCacheableParserContext : BEq CacheableParserContext

Equations

• Lean.Parser.instBEqCacheableParserContext = { beq := Lean.Parser.instBEqCacheableParserContext.beq }

structure Lean.Parser.ParserContextCoreextends Lean.Parser.InputContext, Lean.Parser.ParserModuleContext, Lean.Parser.CacheableParserContext : Type

Parser context updateable in adaptUncacheableContextFn.

• inputString : String
• fileName : String
• fileMap : FileMap
• endPos : String.Pos
• endPos_valid : self.endPos ≤ self.inputString.endPos
• env : Environment
• options : Options
• currNamespace : Name
• openDecls : List OpenDecl
• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token
• tokens : TokenTable

structure Lean.Parser.ParserContextextends Lean.Parser.ParserContextCore : Type

Opaque parser context updateable using adaptCacheableContextFn and adaptUncacheableContextFn.

• inputString : String
• fileName : String
• fileMap : FileMap
• endPos : String.Pos
• endPos_valid : self.endPos ≤ self.inputString.endPos
• env : Environment
• options : Options
• currNamespace : Name
• openDecls : List OpenDecl
• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token
• tokens : TokenTable

instance Lean.Parser.instCoeParserContextInputContext : Coe ParserContext InputContext

Equations

• Lean.Parser.instCoeParserContextInputContext = { coe := fun (x : Lean.Parser.ParserContext) => x.toInputContext }

def Lean.Parser.ParserContext.setEndPos (c : ParserContext) (endPos : String.Pos) (endPos_valid : endPos ≤ c.inputString.endPos) : ParserContext

Modifies the ending position of a parser context.

Equations

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

structure Lean.Parser.Error : Type

• unexpectedTk : Syntax

  If not missing, used for lazily calculating unexpected message and range in mkErrorMessage. Otherwise, ParserState.pos is used as an empty range.

• unexpected : String
• expected : List String

instance Lean.Parser.instInhabitedError : Inhabited Error

Equations

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

def Lean.Parser.instInhabitedError.default : Error

Equations

• Lean.Parser.instInhabitedError.default = { unexpectedTk := default, unexpected := default, expected := default }

def Lean.Parser.instBEqError.beq : Error → Error → Bool

Equations

• Lean.Parser.instBEqError.beq { unexpectedTk := a, unexpected := a_1, expected := a_2 } { unexpectedTk := b, unexpected := b_1, expected := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Parser.instBEqError.beq x✝¹ x✝ = false

instance Lean.Parser.instBEqError : BEq Error

Equations

• Lean.Parser.instBEqError = { beq := Lean.Parser.instBEqError.beq }

def Lean.Parser.Error.toString (e : Error) : String

Equations

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

instance Lean.Parser.Error.instToString : ToString Error

Equations

• Lean.Parser.Error.instToString = { toString := Lean.Parser.Error.toString }

def Lean.Parser.Error.merge (e₁ e₂ : Error) : Error

Equations

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

structure Lean.Parser.TokenCacheEntry : Type

• startPos : String.Pos
• stopPos : String.Pos
• token : Syntax

structure Lean.Parser.ParserCacheKeyextends Lean.Parser.CacheableParserContext : Type

• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? : Option String.Pos
• forbiddenTk? : Option Token
• parserName : Name
• pos : String.Pos

instance Lean.Parser.instBEqParserCacheKey : BEq ParserCacheKey

Equations

• Lean.Parser.instBEqParserCacheKey = { beq := Lean.Parser.instBEqParserCacheKey.beq }

def Lean.Parser.instBEqParserCacheKey.beq : ParserCacheKey → ParserCacheKey → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Parser.instBEqParserCacheKey.beq x✝¹ x✝ = false

instance Lean.Parser.instHashableParserCacheKey : Hashable ParserCacheKey

Equations

• Lean.Parser.instHashableParserCacheKey = { hash := fun (k : Lean.Parser.ParserCacheKey) => hash (k.pos, k.parserName) }

structure Lean.Parser.ParserCacheEntry : Type

• stx : Syntax
• lhsPrec : Nat
• newPos : String.Pos
• errorMsg : Option Error

structure Lean.Parser.ParserCache : Type

• tokenCache : TokenCacheEntry
• parserCache : Std.HashMap ParserCacheKey ParserCacheEntry

def Lean.Parser.initCacheForInput (input : String) : ParserCache

Equations

• Lean.Parser.initCacheForInput input = { tokenCache := { startPos := input.endPos + ' ' }, parserCache := ∅ }

structure Lean.Parser.SyntaxStack : Type

A syntax array with an inaccessible prefix, used for sound caching.

• raw : Array Lean.Syntax
• drop : Nat

def Lean.Parser.SyntaxStack.toSubarray (stack : SyntaxStack) : Subarray Syntax

Equations

• stack.toSubarray = (Lean.Parser.SyntaxStack.raw✝ stack).toSubarray (Lean.Parser.SyntaxStack.drop✝ stack)

def Lean.Parser.SyntaxStack.empty : SyntaxStack

Equations

• Lean.Parser.SyntaxStack.empty = { raw := #[], drop := 0 }

def Lean.Parser.SyntaxStack.size (stack : SyntaxStack) : Nat

Equations

• stack.size = (Lean.Parser.SyntaxStack.raw✝ stack).size - Lean.Parser.SyntaxStack.drop✝ stack

def Lean.Parser.SyntaxStack.isEmpty (stack : SyntaxStack) : Bool

Equations

• stack.isEmpty = (stack.size == 0)

def Lean.Parser.SyntaxStack.shrink (stack : SyntaxStack) (n : Nat) : SyntaxStack

Equations

• stack.shrink n = { raw := (Lean.Parser.SyntaxStack.raw✝ stack).shrink (Lean.Parser.SyntaxStack.drop✝ stack + n), drop := Lean.Parser.SyntaxStack.drop✝¹ stack }

def Lean.Parser.SyntaxStack.push (stack : SyntaxStack) (a : Syntax) : SyntaxStack

Equations

• stack.push a = { raw := (Lean.Parser.SyntaxStack.raw✝ stack).push a, drop := Lean.Parser.SyntaxStack.drop✝ stack }

def Lean.Parser.SyntaxStack.pop (stack : SyntaxStack) : SyntaxStack

Equations

• stack.pop = if stack.size > 0 then { raw := (Lean.Parser.SyntaxStack.raw✝ stack).pop, drop := Lean.Parser.SyntaxStack.drop✝ stack } else stack

def Lean.Parser.SyntaxStack.back (stack : SyntaxStack) : Syntax

Equations

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

def Lean.Parser.SyntaxStack.get! (stack : SyntaxStack) (i : Nat) : Syntax

Equations

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

def Lean.Parser.SyntaxStack.extract (stack : SyntaxStack) (start stop : Nat) : Array Syntax

Equations

• stack.extract start stop = (Lean.Parser.SyntaxStack.raw✝ stack).extract (Lean.Parser.SyntaxStack.drop✝ stack + start) (Lean.Parser.SyntaxStack.drop✝¹ stack + stop)

instance Lean.Parser.SyntaxStack.instHAppendArraySyntax : HAppend SyntaxStack (Array Syntax) SyntaxStack

Equations

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

structure Lean.Parser.ParserState : Type

• stxStack : SyntaxStack
• lhsPrec : Nat

  Set to the precedence of the preceding (not surrounding) parser by runLongestMatchParser for the use of checkLhsPrec in trailing parsers. Note that with chaining, the preceding parser can be another trailing parser: in 1 * 2 + 3, the preceding parser is '*' when '+' is executed.

• pos : String.Pos
• cache : ParserCache
• errorMsg : Option Error
• recoveredErrors : Array (String.Pos × SyntaxStack × Error)

@[inline]

def Lean.Parser.ParserState.hasError (s : ParserState) : Bool

Equations

• s.hasError = (s.errorMsg != none)

def Lean.Parser.ParserState.stackSize (s : ParserState) : Nat

Equations

• s.stackSize = s.stxStack.size

def Lean.Parser.ParserState.restore (s : ParserState) (iniStackSz : Nat) (iniPos : String.Pos) : ParserState

Equations

• s.restore iniStackSz iniPos = { stxStack := s.stxStack.shrink iniStackSz, lhsPrec := s.lhsPrec, pos := iniPos, cache := s.cache, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.setPos (s : ParserState) (pos : String.Pos) : ParserState

Equations

• s.setPos pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.setCache (s : ParserState) (cache : ParserCache) : ParserState

Equations

• s.setCache cache = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.pushSyntax (s : ParserState) (n : Syntax) : ParserState

Equations

• s.pushSyntax n = { stxStack := s.stxStack.push n, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.popSyntax (s : ParserState) : ParserState

Equations

• s.popSyntax = { stxStack := s.stxStack.pop, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.shrinkStack (s : ParserState) (iniStackSz : Nat) : ParserState

Equations

• s.shrinkStack iniStackSz = { stxStack := s.stxStack.shrink iniStackSz, lhsPrec := s.lhsPrec, pos := s.pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.next (s : ParserState) (c : ParserContext) (pos : String.Pos) : ParserState

Equations

• s.next c pos = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := c.next pos, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.next' (s : ParserState) (c : ParserContext) (pos : String.Pos) (h : ¬c.atEnd pos = true) : ParserState

Equations

• s.next' c pos h = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := c.next' pos h, cache := s.cache, errorMsg := s.errorMsg, recoveredErrors := s.recoveredErrors }

def Lean.Parser.ParserState.mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState

Equations

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

def Lean.Parser.ParserState.mkTrailingNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState

Equations

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

def Lean.Parser.ParserState.allErrors (s : ParserState) : Array (String.Pos × SyntaxStack × Error)

Equations

• s.allErrors = s.recoveredErrors ++ (Option.map (fun (e : Lean.Parser.Error) => #[(s.pos, s.stxStack, e)]) s.errorMsg).getD #[]

@[inline]

def Lean.Parser.ParserState.setError (s : ParserState) (e : Error) : ParserState

Equations

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

def Lean.Parser.ParserState.mkError (s : ParserState) (msg : String) : ParserState

Equations

• s.mkError msg = (s.setError { expected := [msg] }).pushSyntax Lean.Syntax.missing

def Lean.Parser.ParserState.mkUnexpectedError (s : ParserState) (msg : String) (expected : List String := []) (pushMissing : Bool := true) : ParserState

Equations

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

def Lean.Parser.ParserState.mkEOIError (s : ParserState) (expected : List String := []) : ParserState

Equations

• s.mkEOIError expected = s.mkUnexpectedError "unexpected end of input" expected

def Lean.Parser.ParserState.mkErrorsAt (s : ParserState) (ex : List String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState

Equations

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

def Lean.Parser.ParserState.mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) (initStackSz? : Option Nat := none) : ParserState

Equations

• s.mkErrorAt msg pos initStackSz? = s.mkErrorsAt [msg] pos initStackSz?

def Lean.Parser.ParserState.mkUnexpectedTokenErrors (s : ParserState) (ex : List String) (iniPos : String.Pos := 0) : ParserState

Reports given 'expected' messages at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

Equations

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

def Lean.Parser.ParserState.mkUnexpectedTokenError (s : ParserState) (msg : String) (iniPos : String.Pos := 0) : ParserState

Reports given 'expected' message at range of top stack element (assumed to be a single token). Replaces the element with missing and resets position to the token position. iniPos can be specified to avoid this position lookup but still must be identical to the token position.

Equations

• s.mkUnexpectedTokenError msg iniPos = s.mkUnexpectedTokenErrors [msg] iniPos

def Lean.Parser.ParserState.mkUnexpectedErrorAt (s : ParserState) (msg : String) (pos : String.Pos) : ParserState

Equations

• s.mkUnexpectedErrorAt msg pos = (s.setPos pos).mkUnexpectedError msg

def Lean.Parser.ParserState.toErrorMsg (ctx : InputContext) (s : ParserState) : String

Equations

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

def Lean.Parser.ParserFn : Type

Equations

• Lean.Parser.ParserFn = (Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState)

instance Lean.Parser.instInhabitedParserFn : Inhabited ParserFn

Equations

• Lean.Parser.instInhabitedParserFn = { default := fun (x : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => s }

inductive Lean.Parser.FirstTokens : Type

• epsilon : FirstTokens
• unknown : FirstTokens
• tokens : List Token → FirstTokens
• optTokens : List Token → FirstTokens

def Lean.Parser.instInhabitedFirstTokens.default : FirstTokens

Equations

• Lean.Parser.instInhabitedFirstTokens.default = Lean.Parser.FirstTokens.epsilon

instance Lean.Parser.instInhabitedFirstTokens : Inhabited FirstTokens

Equations

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

def Lean.Parser.FirstTokens.seq : FirstTokens → FirstTokens → FirstTokens

Equations

• Lean.Parser.FirstTokens.epsilon.seq x✝ = x✝
• (Lean.Parser.FirstTokens.optTokens s₁).seq (Lean.Parser.FirstTokens.optTokens s₂) = Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂)
• (Lean.Parser.FirstTokens.optTokens s₁).seq (Lean.Parser.FirstTokens.tokens s₂) = Lean.Parser.FirstTokens.tokens (s₁ ++ s₂)
• x✝¹.seq x✝ = x✝¹

def Lean.Parser.FirstTokens.toOptional : FirstTokens → FirstTokens

Equations

• (Lean.Parser.FirstTokens.tokens tks).toOptional = Lean.Parser.FirstTokens.optTokens tks
• x✝.toOptional = x✝

def Lean.Parser.FirstTokens.merge : FirstTokens → FirstTokens → FirstTokens

Equations

• Lean.Parser.FirstTokens.epsilon.merge x✝ = x✝.toOptional
• x.merge Lean.Parser.FirstTokens.epsilon = x.toOptional
• (Lean.Parser.FirstTokens.tokens s₁).merge (Lean.Parser.FirstTokens.tokens s₂) = Lean.Parser.FirstTokens.tokens (s₁ ++ s₂)
• (Lean.Parser.FirstTokens.optTokens s₁).merge (Lean.Parser.FirstTokens.optTokens s₂) = Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂)
• (Lean.Parser.FirstTokens.tokens s₁).merge (Lean.Parser.FirstTokens.optTokens s₂) = Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂)
• (Lean.Parser.FirstTokens.optTokens s₁).merge (Lean.Parser.FirstTokens.tokens s₂) = Lean.Parser.FirstTokens.optTokens (s₁ ++ s₂)
• x✝¹.merge x✝ = Lean.Parser.FirstTokens.unknown

def Lean.Parser.FirstTokens.toStr : FirstTokens → String

Equations

• Lean.Parser.FirstTokens.epsilon.toStr = "epsilon"
• Lean.Parser.FirstTokens.unknown.toStr = "unknown"
• (Lean.Parser.FirstTokens.tokens tks).toStr = toString tks
• (Lean.Parser.FirstTokens.optTokens tks).toStr = "?" ++ toString tks

instance Lean.Parser.FirstTokens.instToString : ToString FirstTokens

Equations

• Lean.Parser.FirstTokens.instToString = { toString := Lean.Parser.FirstTokens.toStr }

structure Lean.Parser.ParserInfo : Type

• collectTokens : List Token → List Token
• collectKinds : SyntaxNodeKindSet → SyntaxNodeKindSet
• firstTokens : FirstTokens

instance Lean.Parser.instInhabitedParserInfo : Inhabited ParserInfo

Equations

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

def Lean.Parser.instInhabitedParserInfo.default : ParserInfo

Equations

• Lean.Parser.instInhabitedParserInfo.default = { collectTokens := default, collectKinds := default, firstTokens := default }

structure Lean.Parser.Parser : Type

• info : ParserInfo
• fn : ParserFn

instance Lean.Parser.instInhabitedParser : Inhabited Parser

Equations

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

def Lean.Parser.instInhabitedParser.default : Parser

Equations

• Lean.Parser.instInhabitedParser.default = { info := default, fn := default }

@[reducible, inline]

abbrev Lean.Parser.TrailingParser : Type

Equations

• Lean.Parser.TrailingParser = Lean.Parser.Parser

@[inline]

def Lean.Parser.withFn (f : ParserFn → ParserFn) (p : Parser) : Parser

Create a simple parser combinator that inherits the info of the nested parser.

Equations

• Lean.Parser.withFn f p = { info := p.info, fn := f p.fn }

def Lean.Parser.adaptCacheableContextFn (f : CacheableParserContext → CacheableParserContext) (p : ParserFn) : ParserFn

Equations

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

def Lean.Parser.adaptCacheableContext (f : CacheableParserContext → CacheableParserContext) : Parser → Parser

Equations

• Lean.Parser.adaptCacheableContext f = Lean.Parser.withFn (Lean.Parser.adaptCacheableContextFn f)

def Lean.Parser.withResetCacheFn (p : ParserFn) : ParserFn

Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

Equations

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

def Lean.Parser.withResetCache : Parser → Parser

Run p with a fresh cache, restore outer cache afterwards. p may access the entire syntax stack.

Equations

• Lean.Parser.withResetCache = Lean.Parser.withFn Lean.Parser.withResetCacheFn

def Lean.Parser.adaptUncacheableContextFn (f : ParserContextCore → ParserContextCore) (p : ParserFn) : ParserFn

Run p under the given context transformation with a fresh cache (see also withResetCacheFn).

Equations

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

def Lean.Parser.withCacheFn (parserName : Name) (p : ParserFn) : ParserFn

Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

Equations

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

def Lean.Parser.withCache (parserName : Name) : Parser → Parser

Run p and record result in parser cache for any further invocation with this parserName, parser context, and parser state. p cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history. As this excludes trailing parsers from being cached, we also reset lhsPrec, which is not read but set by leading parsers, to 0 in order to increase cache hits. Finally, errorMsg is also reset to none as a leading parser should not be called in the first place if there was an error.

Equations

• Lean.Parser.withCache parserName = Lean.Parser.withFn (Lean.Parser.withCacheFn parserName)

def Lean.Parser.ParserFn.run (p : ParserFn) (ictx : InputContext) (pmctx : ParserModuleContext) (tokens : TokenTable) (s : ParserState) : ParserState

Equations

• p.run ictx pmctx tokens s = p { toInputContext := ictx, toParserModuleContext := pmctx, prec := 0, tokens := tokens } s