syntax - “|- *中的红色”的用法：连字符星号是什么意思？

Question

在很多 Coq 代码中，比如在标准库中的集合定义中，我看到过这种表示法：

 red in |- *.

|-*(bar-hyphen-star) 是什么意思？

我的搜索没有出现任何结果，但是标点符号很难搜索，所以如果这是重复的，请见谅！

Answer 1

它被称为发生子句，并且

出现子句的作用是选择一个术语在目标中出现的集合。

我会在上面的引用中添加“将要应用该策略”（Coq 参考手册，第 8.1.4 节）。

然后手册继续以下内容：

如果*的右侧提到 ，则|-必须选择目标结论的出现次数。

我们来看一些简单的案例：

• <tactic> in * |-.适用<tactic>于所有假设，但不适用于当前目标。

• <tactic> in H1, H2 |- *.仅适用<tactic>于假设H1和H2 目标。

• <tactic> in * |- *.适用于<tactic>任何地方。这种情况还有一个捷径：<tactic> in *.

对于很多战术<tactic> in |- *.来说，就相当于刚刚<tactic>。例如，如果您in |- *从链接文件中删除所有出现的 ，它仍然会编译。