Как вы смотрите, где идентификаторы определены в Coq эффективно?

Question

В большинстве IDE или текстовых редакторах вы можете щелкнуть правой кнопкой мыши по термину и передать его в файл, где этот термин определен. CoqIDE, похоже, не имеет этого, поэтому я делал coqdoc myfile.v --html, а затем перешел к сгенерированным документам HTML. Но единственные доступные для клика условия этого файла для стандартной библиотеки Coq. Термины, определенные ssreflect (например), не доступны для кликов.

Есть ли стандартный способ быстрого поиска, где определенный член/идентификатор определен (и его исходный код), когда в файле Coq? Либо в CoqIDE, либо в emacs + ProofGeneral (я использую CoqIDE, но я бы переключился, если emacs/ProofGeneral имел эту способность).

Или стандартный способ создания документов для каждого проекта Coq и зависимости, которую вы используете?

Answer 1

Если вы выделили термин и выполните Запросы -> Найти, или вы оцените Locate some_identifier., вы получите полное имя константы. Если вы знаете, где установлены зависимости, это скажет вам, где искать идентификатор.

Редактировать: Если вы хотите определить идентификатор, вы можете Print его. Если вы просто хотите его тип, вы можете использовать About, или Check (который также принимает выражения, а не только идентификаторы).

Answer 2

Существует инструмент, работающий на верхней части доказательства, называемый company-coq. Он имеет функцию перехода к определению, привязанную к ярлыку клавиатуры M-. по умолчанию.

Он может перейти к определению под курсором (даже к стандартной библиотеке), только если модуль, содержащий определение, требуется с помощью команды Require или ее варианта.