Geek Answers Handbook

Definition of the definition of tactics in Coq evidence

When studying the accompanying evidence of other authors, I often come across tactics such as inv eq Heq or intro_b. I want to understand this tactic.

How can I find if it is Coq tactical tactics or tactical notation defined somewhere in my current project?

Secondly, is there a way to find my definition?

I used SearchAbout, Search, Locate and Print, but could not find the answers to the above questions.

+6
source share
2 answers

You should be able to use

Print Ltac <tacticname>.

to print custom tactics code (as per documentation ).

To find where this is defined ... I think you will need grep, unfortunately Locate does not work for tactic names.

+4
source

As mentioned earlier, Print Ltac ... prints custom tactics code.

To find a user-defined tactic (that is, know where it is defined), use Locate Ltac ... This gives you the full name. Then use the Locate Library to find the appropriate file.

+2
source

More articles:


All Articles