複数の仮説を一度にクリアする戦術が欲しいとします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).
私の質問は、Prods を使用せずにそれを行う方法ですか?
この質問を確認しましたが、必要な引数の数がわからないため、正確には必要ありません。