Как вы смотрите, где идентификаторы определены в Coq эффективно?
В большинстве IDE или текстовых редакторов вы можете щелкнуть правой кнопкой мыши термин, и он приведет вас к файлу, в котором этот термин определен. У CoqIDE этого нет, поэтому я занимаюсь coqdoc myfile.v --htmlЗатем перейдем к сгенерированным документам HTML. Но единственные кликабельные термины в этом файле относятся к стандартной библиотеке Coq. Термины, определенные ssreflect (например), не кликабельны.
Существует ли стандартный способ быстрого поиска, где определен какой-либо термин / идентификатор (и исходный код для него) в файле Coq? Либо в CoqIDE, либо в emacs + ProofGeneral (я использую CoqIDE, но я бы переключился, если бы у emacs/ProofGeneral была такая возможность).
Или это стандартный способ создания документов для каждого проекта Coq и зависимости, которую вы используете?
2 ответа
Если вы выделите термин и выполните Queries -> Locate, или вы оцениваете Locate some_identifier., вы получите полное имя константы. Если вы знаете, где установлены зависимости, это скажет вам, где искать идентификатор.
Редактировать: если вы хотите определить идентификатор, вы можете Print Это. Если вы просто хотите его тип, вы можете использовать About, или же Check (который также принимает выражения, а не только идентификаторы).
В дополнение к Proof General есть инструмент под названием company-coq. Он имеет функцию перехода к определению, привязанную к M-. сочетание клавиш по умолчанию.
Он может перейти к определению под курсором (даже к стандартной библиотеке), только если модуль, содержащий определение, требуется с Require команда или ее вариант.