Тактика 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. *)
Примечание: я знаюсоздание экземпляра по позиции не рекомендуется, но я использую свою тактику только для целей исследования.