参考 Ltac 中的 hintbases

Question

在我的项目中，我试图维护小型提示库以加快证明速度。然而，当我为此类架构编写 Ltac 支持时，我找不到引用各种提示库的方法。本质上，我想执行以下操作：

Tactic Notation "myauto" ???(db) := auto with db.

会比这更复杂。但是，Coq 解析器似乎急切地将 db 解析为提示库的具体名称，因此会抛出这样的错误消息：

Error: No such Hint database: db.

有什么方法可以参数化 auto 系列的提示基础选项？

Answer 1

编辑：

您正在尝试执行的操作目前在 Ltac 中不起作用。

https://github.com/coq/coq/issues/2417

您可以通过以下任一方式解决您的问题

• 将您的问题改写成一个单独的问题，在其中解释为什么需要这种自动化，有人可能会以不同的方式帮助您解决最初的问题（不使用自动和数据库参数）

或

• 试用较新的 Coq 策略库之一，例如 Ltac2

---

旧（损坏）答案：

在 Coq 8.7.2 中，您正在寻找的是 ident 参数类型。 根据定义，Hint 数据库由 ident:

引用

Create HintDb ident [discriminated] 

（定义见https://coq.inria.fr/distrib/current/refman/tactics.html#Hints-databases）

放

Tactic Notation "test" ident(db) :=
  auto with db.

适合我。

https://coq.inria.fr/distrib/current/refman/syntax-extensions.html#hevea_command236 包含允许的修饰符列表。