syntax - "red in |- *": What does bar hyphen star mean? 的用法

Question

在很多 Coq 代码中，比如 the definition of sets在标准库中，我见过这种表示法:

 red in |- *.

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

我的搜索没有找到任何结果，但是标点符号很难搜索，所以如果重复，请原谅!

Answer 1

它被称为出现条款 和

The role of an occurrence clause is to select a set of occurrences of a term in a goal.

我会在上面的引述(Coq 引用手册，sect. 8.1.4)中添加“将要应用该策略的对象”。

然后手册继续执行以下操作:

if * is mentioned on the right of |-, the occurrences of the conclusion of the goal have to be selected.

让我们看一些简单的案例:

• <tactic> in * |-.适用 <tactic>每个假设，但不是当前目标。

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

• <tactic> in * |- *.适用 <tactic>到处。这种情况还有一个快捷方式:<tactic> in * .

对于许多策略<tactic> in |- *.相当于 <tactic> .例如，如果您删除所有出现的 in |- *从链接文件中它仍然会编译。