core / init.meta.lean.parser
Make sure the next token is an identifier, consume it, and
produce the quoted name `t, where t is the identifier.
Make sure the next token is a small nat, consume it, and produce it
Check that the next token is tk and consume it. tk must be a registered token.
Parse an unelaborated expression using the given right-binding power.
When pat := tt, the expression is parsed as a pattern, i.e. local
constants are not checked.
pat := tt
a variable to local scope
Run the parser in a local declaration scope.
Local declarations added via add_local do not propagate outside of this scope.
Parse an interactive tactic block: begin .. end
Do not report info from content parsed by p.
Set goal info position of content parsed by p to current position. Nested calls take precedence.
Return the current parser position without consuming any input.
Temporarily replace input of the parser state, run p, and return remaining input.
Parse a top-level command.