可変アリティを持つ戦術

Question

と言っていいでしょう。clear_multiple H1, H2, H3.のようなことをするために、一度に複数の仮説をクリアするための戦術を持ちたいとします。私は、次のように、ペアを使用していることを実行しようとしました：

Ltac clear_multiple arg := 
match arg with 
| (?f, ?s) => clear s; clear_multiple f 
| ?f => clear f 
end. 

しかし、その後、問題は、私はProdを持つように括弧を配置しなければならないということです。

Variable A: Prop. 

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

私の質問を行う方法であり、それはProdを使わずに？

---

私は this questionをチェックしますが、私が欲しいの引数の数が知られていないので、それは、まさに私が欲しいものではありません。

Answer 1

clear戦術は複数の引数を取ることができるので、新しい戦術を定義する必要はありません。clear H H0 H1と書くことができます。

もちろん、他のタスクのためにこのようなn-ary戦術を定義することもできます。 Coqには、このような定義をサポートするtactic notation mechanismがあります。残念なことに、あまりにも強力ではありません。特定の種類の引数のリストを、複数の引数（たとえば、clear）を必要とする戦略に渡すことができます。私はそれがあなたがプログラムで反復できるリストを与えることはできないと思います。