Как я могу найти, в каком файле определено значение?

Question

Когда я работаю над доказательством Coq, я часто хочу найти, из какого файла происходит определение.

например. У меня была цель, которая содержит list_norepet (map fst (PTree.elements ta)), и я хотел найти файл, который определил list_norepet. Выполнение Print list_norepet. показывает много полезной информации, но не имя файла. Есть ли способ заставить Coq напечатать это?

Answer 1

Вы можете использовать Locate, чтобы получить полное имя модуля. Обычно этого достаточно, чтобы найти файл, но тогда вы можете использовать Locate File, чтобы попытаться найти его:

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

Я говорю «попробуй найти», потому что вам нужно знать переназначения (с -R), чтобы можно было преобразовывать пути модулей в пути к файлам - например, стандартная библиотека Coq находится в theories, но отображается до Coq.