在Coq样张中定位策略的定义

Question

在研究其他作者的Coq证明时,我经常遇到一种策略,让我们说"inv eq Heq"或"intro_b".我想了解这样的策略.

如何在我当前的项目中找到某个Coq策略或战术符号？

第二,有没有办法找到它的定义？

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

Answer 1

你应该能够使用

Print Ltac <tacticname>.

打印用户定义策略的代码（根据文档）。

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