代码之家 › 专栏 › 技术社区 › Jason Hu

参见Ltac中的Hintbase

coq-tactic coq

2

Jason Hu · 技术社区 · 8 年前

在我的项目中,我试图维护小型hintbase,以加快证明速度。然而,当我编写这种体系结构的Ltac支持时,我找不到一种方法来引用各种hintbase。基本上,我想做以下工作:

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

这将比那更复杂。然而,Coq解析器似乎热衷于解析 db 作为提示库的具体名称,因此将引发如下错误消息:

Error: No such Hint database: db.

我可以通过任何方式参数化 auto 家庭

1 回复 | 直到 8 年前

1

2

Heiko Becker 8 年前

编辑:

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

你可以通过

或

旧(坏)答案:

在Coq 8.7.2中,您需要的是 ident 参数类型。根据定义,提示数据库由 识别号 :

Create HintDb ident [discriminated]

放置

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

对我来说很好。