mathlib documentation

core / init.meta.lean.parser

meta constant lean.parser_state  :
Type
@[reducible]
meta def lean.parser (α : Type u_1) :
Type u_1
@[reducible]
meta def lean.parser_result (α : Type u_1) :
Type u_1
meta def lean.parser.val {α : Type} (p : lean.parser (reflected_value α)) :
Instances for lean.parser.val
meta def lean.parser.reflectable.expr {α : Type} {p : lean.parser α} (r : p.reflectable) :
meta def lean.parser.reflectable.to_parser {α : Type} {p : lean.parser α} (r : p.reflectable) :
meta constant lean.parser.ident  :

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

meta constant lean.parser.tk (tk : string) :

Check that the next token is tk and consume it. tk must be a registered token.

@[protected]
meta constant lean.parser.pexpr (rbp : := std.prec.max) (pat : bool := bool.ff) :

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.

meta constant lean.parser.add_local (v : expr) :

a variable to local scope

meta def lean.parser.with_local_scope {α : Type} (p : lean.parser α) :

Run the parser in a local declaration scope.

Local declarations added via add_local do not propagate outside of this scope.

@[protected, reducible]

Parse an interactive tactic block: begin .. end

meta constant lean.parser.skip_info {α : Type} (p : lean.parser α) :

Do not report info from content parsed by p.

meta constant lean.parser.set_goal_info_pos {α : Type} (p : lean.parser α) :

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.

meta constant lean.parser.with_input {α : Type} (p : lean.parser α) (input : string) :

Temporarily replace input of the parser state, run p, and return remaining input.

Parse a top-level command.

meta def lean.parser.parser_orelse {α : Type} (p₁ p₂ : lean.parser α) :
@[protected, instance]
meta def lean.parser.many {f : Type uType v} [monad f] [alternative f] {a : Type u} :
f af (list a)
meta def lean.parser.sep_by {α : Type} :
meta constant lean.parser.of_tactic {α : Type} :
@[protected, instance]
meta def lean.parser.has_coe {α : Type} :
@[protected, instance]
@[protected, instance]
meta def lean.parser.reflectable.has_reflect {α : Type} [r : has_reflect α] (p : lean.parser α) :
@[protected, instance]
meta def lean.parser.reflectable.optional {α : Type} [reflected Type α] (p : lean.parser α) [r : p.reflectable] :
meta def lean.parser.reflect {α : Type} (p : lean.parser α) [r : p.reflectable] :
meta constant lean.parser.run {α : Type u_1} :
meta def lean.parser.run_with_input {α : Type} :
lean.parser αstringtactic α