coq で 1 つまたは 3 つの引数を取る Ltac タクティックを作成したいと考えています。モジュールについて読んだことltac_No_argがありLibTacticsますが、それを正しく理解していれば、次の方法で戦術を呼び出す必要があります。
Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.
これはあまり便利ではありません。
このような結果を得る方法はありますか? :
Coq < mytactic arg_1.
Coq < mytactic arg_1 arg_2 arg_3.