mathlib3 documentation

core / init.meta.interactive_base

@[reducible]
meta def interactive.parse {α : Type} (p : lean.parser α) [p.reflectable] :

(parse p) as the parameter type of an interactive tactic will instruct the Lean parser to run p when parsing the parameter and to pass the parsed value as an argument to the tactic.

inductive interactive.loc  :

A loc is either a 'wildcard', which means "everywhere", or a list of option names. none means target and some n means n in the local context.

Instances for interactive.loc
meta def interactive.loc.apply (hyp_tac : expr tactic unit) (goal_tac : tactic unit) (l : interactive.loc) :
meta def interactive.with_desc {α : Type} (desc : format) (p : lean.parser α) :

Use desc as the interactive description of p.

Instances for interactive.with_desc
@[protected, instance]
meta def interactive.types.brackets {α : Type} (l r : string) (p : lean.parser α) :

The right-binding power 2 will terminate expressions by '<|>' (rbp 2), ';' (rbp 1), and ',' (rbp 0). It should be used for any (potentially) trailing expression parameters.

A 'tactic expression', which uses right-binding power 2 so that it is terminated by '<|>' (rbp 2), ';' (rbp 1), and ',' (rbp 0). It should be used for any (potentially) trailing expression parameters.

Parse an identifier or a '_'

meta structure interactive.decl_modifiers  :

Parses and elaborates a single or multiple mutual inductive declarations (without the inductive keyword), depending on is_mutual