用于实例化的Ltac位置参数

Question

策略instantiate可以将ident或num作为：

instantiate (ident:= term)

instantiate (num := term)

现在我想在战术定义中使用第二个。例如：

  Ltac my_instantiate n x:=
    instantiate(n:=x).

不幸的是，这会产生以下错误：

Ltac变量n被绑定到1，这不能强制到一个新的标识符。

我怀疑ltac正在尝试第一次使用instantiate。如何告诉coq按位置实例化，或者如何正确地传递argumetn？

下面是一个很小的例子：

Ltac my_instantiate n x:=
  instantiate(n:=x).
Goal exists x, x = 2.
  eexists.
  my_instantiate 1 2.
  (* Fails with: Ltac variable n is bound to 1 which 
     cannot be coerced to a fresh identifier. *)

注意:我知道不鼓励按位置实例化，但我只是为了探索的目的而使用我的策略。

Answer 1

也许你想要的东西可以用一种战术符号来表达？

参考手册-战术符号