coq - 在 Coq 证明中定位策略的定义

Question

在研究其他作者的 Coq 证明时，我经常遇到一种策略，比如“inv eq Heq”或“intro_b”。我想了解这样的战术。

如何确定它是在我当前项目中的某处定义的 Coq 策略还是 Tactic Notation？

其次，有没有办法找到它的定义？

我使用了 SearchAbout、Search、Locate 和 Print，但找不到上述问题的答案。

Answer 1

你应该可以使用

Print Ltac <tacticname>.

打印用户定义策略的代码(根据 documentation )。

要找到它的定义位置...不幸的是，我想您将需要 grep， Locate似乎不适用于战术名称。