mathlib docs: core.init.meta.lean.parser

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 :

expr → lean.parser unit

a variable to local scope

source

meta constant lean.parser.add_local_level :

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} :

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

meta constant lean.parser.itactic_reflected :

lean.parser (reflected_value (tactic unit))

source

meta def lean.parser.itactic :

lean.parser (tactic unit)

Parse an interactive tactic block: begin .. end

source

meta constant lean.parser.skip_info {α : Type} :

lean.parser α → lean.parser α

Do not report info from content parsed by p.

source

meta constant lean.parser.set_goal_info_pos {α : Type} :

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} :

lean.parser α → 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} :

lean.parser α → lean.parser α → lean.parser α

source

@[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

@[instance]

meta def lean.parser.has_coe {α : Type} :

has_coe (tactic α) (lean.parser α)

source

@[instance]

meta def lean.parser.reflectable.cast {α : Type} (p : lean.parser (reflected_value α)) :

p.val.reflectable

source

@[instance]

meta def lean.parser.reflectable.has_reflect {α : Type} [r : has_reflect α] (p : lean.parser α) :

p.reflectable

source

@[instance]

meta def lean.parser.reflectable.optional {α : Type} [reflected α] (p : lean.parser α) [r : p.reflectable] :

(optional p).reflectable

source

meta def lean.parser.reflect {α : Type} (p : lean.parser α) [r : p.reflectable] :

lean.parser expr

mathlib documentation

core.init.meta.lean.parser

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​meta.​lean.​parser

General documentation

Additional documentation

Library

core.init.meta.lean.parser