(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.
- wildcard : interactive.loc
- ns : list (option name) → 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.
Use desc as the interactive description of p.
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.
- attrs : interactive.decl_attributes
- modifiers : interactive.decl_modifiers
- doc_string : option string
- attrs : interactive.decl_attributes
- sig : expr
- intros : list expr
Parses and elaborates a single or multiple mutual inductive declarations (without the inductive keyword), depending on is_mutual