Variable Tactics

Question

Let's say I want to have a tactic to clear out a few hypotheses at once in order to do something like clear_multiple H1, H2, H3.. I tried to do this with pairs, for example:

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 put the brackets in order to have Prod:

Variable A: Prop.

Goal A -> A -> A -> True.
intros.
clear_multiple (H, H0, H1).

My question is: how to do this without using Prod?

---

I checked this question , but this is not quite what I want, since the number of arguments I want is unknown.

Answer 1

You may like to know that tactics clearcan take several arguments, so you don’t need to define a new tactic: you can just write clear H H0 H1.

, ​​n-ary . Coq , . , : , (, clear); , , .