mathlib documentation

core / init.meta.interactive_base

source
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.

source
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.

source
meta def interactive.loc.include_goal  :
interactive.loc → bool
source
meta def interactive.loc.get_locals  :
interactive.loc → tactic (list expr)
source
meta def interactive.loc.apply (hyp_tac : expr → tactic unit) (goal_tac : tactic unit) (l : interactive.loc) :
tactic unit
source
meta def interactive.loc.try_apply (hyp_tac : expr → tactic unit) (goal_tac : tactic unit) (l : interactive.loc) :
tactic unit
source
meta def interactive.with_desc {α : Type} (desc : format) (p : lean.parser α) :
lean.parser α

Use desc as the interactive description of p.

source
@[protected, instance]
meta def interactive.with_desc.reflectable {α : Type} (p : lean.parser α) [h : p.reflectable] (f : format) :
(interactive.with_desc f p).reflectable
source
meta def interactive.types.brackets {α : Type} (l r : string) (p : lean.parser α) :
lean.parser α
source
meta def interactive.types.list_of {α : Type} (p : lean.parser α) :
lean.parser (list α)
source
meta def interactive.types.tac_rbp  :
ℕ

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.

source
meta def interactive.types.texpr  :
lean.parser pexpr

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.

source
meta def interactive.types.ident_  :
lean.parser name

Parse an identifier or a '_'

source
meta def interactive.types.using_ident  :
lean.parser (option name)
source
meta def interactive.types.with_ident_list  :
lean.parser (list name)
source
meta def interactive.types.without_ident_list  :
lean.parser (list name)
source
meta def interactive.types.location  :
lean.parser interactive.loc
source
meta def interactive.types.pexpr_list  :
lean.parser (list pexpr)
source
meta def interactive.types.opt_pexpr_list  :
lean.parser (list pexpr)
source
meta def interactive.types.pexpr_list_or_texpr  :
lean.parser (list pexpr)
source
meta def interactive.types.only_flag  :
lean.parser bool
source
meta def interactive.param_desc  :
expr → tactic format
source
meta constant interactive.parse_binders_core (rbp : ℕ) :
lean.parser (list pexpr)
source
meta def interactive.parse_binders (rbp : ℕ := std.prec.max) :
lean.parser (list pexpr)
source
meta constant interactive.decl_attributes  :
Type
source
meta constant interactive.decl_attributes.apply  :
interactive.decl_attributes → name → lean.parser unit
source
meta inductive interactive.noncomputable_modifier  :
Type
source
meta structure interactive.decl_modifiers  :
Type
source
meta structure interactive.decl_meta_info  :
Type
source
meta structure interactive.single_inductive_decl  :
Type
source
meta def interactive.single_inductive_decl.name (d : interactive.single_inductive_decl) :
name
source
meta structure interactive.inductive_decl  :
Type
source
meta constant interactive.inductive_decl.parse  :
interactive.decl_meta_info → lean.parser interactive.inductive_decl

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

source
meta def format_macro (_x : interactive.parse (lean.parser.tk "format!")) (s : string) :
lean.parser pexpr
source
meta def sformat_macro (_x : interactive.parse (lean.parser.tk "sformat!")) (s : string) :
lean.parser pexpr