CODEWITHSUNDEEP
coq
Vilhelm Sjöberg
Vilhelm Sjöberg

Reputation: 503

How can I find what file a value is defined in?

When I work on a Coq proof I often want to find which file a definition comes from.

E.g. I had a goal which contains list_norepet (map fst (PTree.elements ta)), and I wanted to find the file that defined list_norepet. Doing Print list_norepet. shows lots of helpful information, but not the file name. Is there any way to get Coq to print that?

Upvotes: 0

Views: 63

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

You can use Locate to get the full module name. Usually this is enough to find the file, but then you can use Locate File to try to find it:

Locate eq_rect.
(* Constant Coq.Init.Logic.eq_rect *)
Locate File "Init/Logic.v".
(* /Users/tchajed/code/sw/coq-master/theories/Init/Logic.v *)

I say "try to find it" because you do need to know the remappings (with -R) to be able to translate module paths to file paths - for example, Coq's standard library is in theories but is mapped to Coq.

Upvotes: 3

Related Questions