# Documentation

Lean.Parser.Types

@[inline]
Equations
@[inline]
Equations
def Lean.Parser.getNext (input : String) (pos : String.Pos) :

Return character after position pos

Equations

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
Equations
Equations
Equations
@[inline]
Equations
@[inline]
Equations
@[inline]
Equations

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.

Instances For
Equations

Input context derived from elaboration of previous commands.

Instances For
• prec : Nat
• quotDepth : Nat
• suppressInsideQuot : Bool
• savedPos? :
• forbiddenTk? :

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

Instances For

Parser context updateable in adaptUncacheableContextFn.

Instances For

Opaque parser context updateable using adaptCacheableContextFn and adaptUncacheableContextFn.

Instances For
• unexpected : String
• expected :
Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Instances For
Instances For
Equations
Equations
Instances For
Equations
• raw :
• drop : Nat

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

Instances For
Equations
Equations
Equations
Equations
• = ()
Equations
• = { raw := Array.shrink stack.raw (stack.drop + n), drop := stack.drop }
Equations
• = { raw := Array.push stack.raw a, drop := stack.drop }
Equations
• = if then { raw := Array.pop stack.raw, drop := stack.drop } else stack
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
• 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.

lhsPrec : Nat
• errorMsg :
Instances For
Equations
• = (s.errorMsg != none)
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := pos, cache := s.cache, errorMsg := s.errorMsg }
Equations
• = { stxStack := s.stxStack, lhsPrec := s.lhsPrec, pos := s.pos, cache := cache, errorMsg := s.errorMsg }
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def Lean.Parser.ParserState.mkUnexpectedError (msg : String) (expected : optParam () []) (pushMissing : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• = match x with | => | tks => tks
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
@[inline]
Equations
@[inline]

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

Equations
• = { info := p.info, fn := f p.fn }
Equations
• One or more equations did not get rendered due to their size.

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.

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

Equations

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

Equations

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 : Lean.Name) :

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
Equations
• One or more equations did not get rendered due to their size.