Generally useful tactics.
Make a PreDefinition taking some metadata from declaration
You can provide a new type, value and (optional) docstring, but the remaining information is taken
Currently only implemented for definitions and theorems. Also see docstring of
Get the array of
FVarIds in the local context of the given
ids is specified, elaborate them in the local context of the given goal to obtain the array of
false (the default), we filter out implementation details
auxDecls) from the resulting list of
Run a tactic on all goals, and always succeeds.
Repeats a tactic at most
n times, stopping sooner if the
tactic fails. Always succeeds.
iterateExactly' n t executes
n times. If any iteration fails, the whole tactic fails.
iterateRange m n t: Repeat the given tactic at least
m times and
n times or until
t fails. Fails if
t does not run at least
iterateUntilFailureWithResults is a helper tactic which accumulates the list of results
obtained from iterating
tac until it fails. Always succeeds.