参考Ltac中的后盾

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

旧(坏)答案：

在CoQ8.7.2中，您要寻找的是ident参数类型。根据定义，提示数据库由ident引用。

Create HintDb ident [discriminated] 

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

推送

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

对我来说很好。

command236包含允许修饰符的列表。