Ltac：任意の引数の戦術

1つまたは3つの引数をとるcoqのLtac戦術を作りたいと思います。私はLibTacticsモジュールでは約ltac_No_argを読みましたが、私はそれを正しく理解している場合、私はと私の戦術を起動する必要があります。非常に便利ではありませんLtac：任意の引数の戦術

Coq < mytactic arg_1 ltac_no_arg ltac_no_arg.

。

このような結果を得る方法はありますか？：

Coq < mytactic arg_1. 

Coq < mytactic arg_1 arg_2 arg_3.

出典

2017-06-30 L. Soret

それは可変長引数を扱うことができるので、私たちはあなたの問題を解決しようとするTactic Notationメカニズムを使用することができます。

Tactic Notation "mytactic_notation" constr(x) := 
    mytactic x ltac_no_arg ltac_no_arg. 
Tactic Notation "mytactic_notation" constr(x) constr(y) constr(z) := 
    mytactic x y z.

テスト：

Goal True. 
    mytactic_notation 1. 
    mytactic_notation 1 2 3. 
Abort.

出典

2017-06-30 08:50:21

は何ですか

Inductive ltac_No_arg : Set := | ltac_no_arg : ltac_No_arg. Ltac mytactic x y z := match type of y with | ltac_No_arg => idtac "x =" x (* a bunch of cases omitted *) | _ => idtac "x =" x "; y =" y "; z =" z end.

は、今度は、前述の戦術表記法を定義してみましょうのはltac_No_argを再利用しようとデモンストレーションの目的でダミー戦術mytacticを定義します'constr（x）'？ Vernacularの 'x'ですか？ – jaam

'Tactic Notation'の引数の型を指定します。ここで、 'constr（x）'は、識別子、整数などではなく、 'x'を解析し解釈することを意味します。 –

[this]（https://coq.inria.fr/refman/Reference-Manual003.html#term）を意味しますか？（例えば、タイプとソートは用語の適切なサブクラスであり、 'qualid'は識別子として定義される用語です） – jaam

答えて

関連する問題