mathlib documentation

core / init.meta.lean.parser

source
meta constant lean.parser_state  :
Type
source
meta constant lean.parser_state.env  :
lean.parser_state → environment
source
meta constant lean.parser_state.options  :
lean.parser_state → options
source
meta constant lean.parser_state.cur_pos  :
lean.parser_state → pos
source
meta def lean.parser (α : Type u_1) :
Type u_1
source
meta def lean.parser_result (α : Type u_1) :
Type u_1
source
meta def lean.parser.val {α : Type} (p : lean.parser (reflected_value α)) :
lean.parser α
source
@[class]
meta structure lean.parser.reflectable {α : Type} (p : lean.parser α) :
Type
Instances
source
meta def lean.parser.reflectable.expr {α : Type} {p : lean.parser α} (r : p.reflectable) :
lean.parser expr
source
meta def lean.parser.reflectable.to_parser {α : Type} {p : lean.parser α} (r : p.reflectable) :
lean.parser α
source
meta def lean.parser.get_env  :
lean.parser environment
source
meta constant lean.parser.set_env  :
environment → lean.parser unit
source
meta constant lean.parser.ident  :
lean.parser name

Make sure the next token is an identifier, consume it, and produce the quoted name `t, where t is the identifier.

source
meta constant lean.parser.small_nat  :
lean.parser ℕ

Make sure the next token is a small nat, consume it, and produce it

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

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

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

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.

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

a variable to local scope

source
meta constant lean.parser.add_local_level (v : name) :
lean.parser unit
source
meta constant lean.parser.list_include_var_names  :
lean.parser (list name)
source
meta constant lean.parser.list_available_include_vars  :
lean.parser (list expr)
source
meta constant lean.parser.include_var  :
name → lean.parser unit
source
meta constant lean.parser.omit_var  :
name → lean.parser unit
source
meta constant lean.parser.push_local_scope  :
lean.parser unit
source
meta constant lean.parser.pop_local_scope  :
lean.parser unit
source
meta def lean.parser.with_local_scope {α : Type} (p : lean.parser α) :
lean.parser α

Run the parser in a local declaration scope.

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

source
@[protected]
meta constant lean.parser.itactic_reflected  :
lean.parser (reflected_value (tactic unit))
source
@[protected]
meta def lean.parser.itactic  :
lean.parser (tactic unit)

Parse an interactive tactic block: begin .. end

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

Do not report info from content parsed by p.

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

Set goal info position of content parsed by p to current position. Nested calls take precedence.

source
meta def lean.parser.cur_pos  :
lean.parser pos

Return the current parser position without consuming any input.

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

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

source
meta constant lean.parser.command_like  :
lean.parser unit

Parse a top-level command.

source
meta def lean.parser.parser_orelse {α : Type} (p₁ p₂ : lean.parser α) :
lean.parser α
source
@[protected, instance]
meta def lean.parser.alternative  :
alternative lean.parser
source
meta def lean.parser.many {f : Type u → Type v} [monad f] [alternative f] {a : Type u} :
f a → f (list a)
source
meta def lean.parser.sep_by {α : Type} :
lean.parser unit → lean.parser α → lean.parser (list α)
source
meta constant lean.parser.of_tactic {α : Type} :
tactic α → lean.parser α
source
@[protected, instance]
meta def lean.parser.has_coe {α : Type} :
has_coe (tactic α) (lean.parser α)
source
@[protected, instance]
meta def lean.parser.reflectable.cast {α : Type} (p : lean.parser (reflected_value α)) :
p.val.reflectable
source
@[protected, instance]
meta def lean.parser.reflectable.has_reflect {α : Type} [r : has_reflect α] (p : lean.parser α) :
p.reflectable
source
@[protected, instance]
meta def lean.parser.reflectable.optional {α : Type} [reflected α] (p : lean.parser α) [r : p.reflectable] :
p?.reflectable
source
meta def lean.parser.reflect {α : Type} (p : lean.parser α) [r : p.reflectable] :
lean.parser expr
source
meta constant lean.parser.run {α : Type u_1} :
lean.parser α → tactic α
source
meta def lean.parser.run_with_input {α : Type} :
lean.parser α → string → tactic α