mathlib documentation

core / init.meta.interactive_base

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

(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  :
Type

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 : exprtactic unit) (goal_tac : tactic unit) (l : interactive.loc) :
meta def interactive.loc.try_apply (hyp_tac : exprtactic 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 α) :
meta def interactive.types.list_of {α : Type} (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 constant interactive.decl_attributes  :
Type
meta structure interactive.decl_modifiers  :
Type
meta structure interactive.single_inductive_decl  :
Type
meta structure interactive.inductive_decl  :
Type

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