Say I want to have a tactic to clear multiple hypothesis at once, to do something like clear_multiple H1, H2, H3.. I tried to do that using pairs, like the following:
Ltac clear_multiple arg :=
match arg with
| (?f, ?s) => clear s; clear_multiple f
| ?f => clear f
end.
But then, the problem is that I have to place parenthesis to have a Prod:
Variable A: Prop.
Goal A -> A -> A -> True.
intros.
clear_multiple (H, H0, H1).
My question is, how to do that without using Prods ?
I checked this question, but it is not exactly what I want, since the number of arguments I want is not known.
You might like to know that the clear tactic can take multiple arguments, so you do not need to define a new tactic: you can just write clear H H0 H1.
Of course, you might want to define such n-ary tactics for other tasks. Coq has a tactic notation mechanism that supports such definitions. Unfortunately, they are not too powerful: you can only pass a list of arguments of a certain kind to a tactic that expects multiple arguments (like clear); I don't think it can give you a list that you can iterate on programmatically.