Просмотреть определение в Coq-IDE - PullRequest
Новая
       66

Просмотреть определение в Coq-IDE

0 голосов
/ 26 января 2020

В помощнике по проверке Изабель можно щелкнуть Ctrl + щелчок по термину, и среда IDE перенаправит его на соответствующее определение.

Можно ли это сделать с помощью CoqIde? С генеральным доказательством?

1 Ответ

1 голос
/ 27 января 2020

Да, функции, которые вы упомянули в своем посте и в своем комментарии (помимо этого, не стесняйтесь редактировать свой вопрос, чтобы включить свой комментарий), возможны в Proof-General и / или company-coq (пакет Emacs, в котором собраны расширения IDE Proof-General):

  • для просмотра содержания определения def (эквивалент Print def. ): C - c C -a C -p def RET
  • , чтобы увидеть тип определения def (эквивалент Check def.): C - c C -a C - c def RET
  • для просмотра типа и связанных метаданных определения def (эквивалент About def.): C - c C -a C -b def RET
  • , чтобы увидеть все это в одном go для идентификатора под точкой (требуется company-coq ): C - c C -d
  • для быть перенаправлен на место определения под точкой (требуется company-coq ): M -. * 104 1 *
  • , чтобы определение под точкой отображалось без движения (требуется company-coq ):

Напоминания

Просто чтобы быть автономными, сочетания клавиш Emacs C - c, M -. , RET , см. Ctrl + c, Alt +. , Return и Ctrl + щелчок (без отпускания кнопки мыши).

Наконец, вы можете найти список привязок, связанных с окружающим режимом, выполнив C -hm :

C -hk [describe-key] C -hm [describe-mode]: 

C-h m runs the command describe-mode (found in global-map), which is
an interactive compiled Lisp function in ‘help.el’.

It is bound to C-h m, <f1> m, <help> m, <menu-bar> <help-menu>
<describe> <describe-mode>.

(describe-mode &optional BUFFER)

Display documentation of current major mode and minor modes.
A brief summary of the minor modes comes first, followed by the
major mode description.  This is followed by detailed
descriptions of the minor modes, each on a separate page.

[…]
...