CODEWITHSUNDEEP
emacscoqcoqideproof-general
Lance Pollard
Lance Pollard

Reputation: 79238

How do you look up where identifiers are defined in Coq efficiently?

In most IDEs or text editors, you can right-click a term and it takes you to the file where that term is defined. CoqIDE doesn't seem to have that, so I've been doing coqdoc myfile.v --html, then going to the generated HTML docs. But the only clickable terms in that file are for Coq Standard Library. Terms defined by ssreflect (for example) aren't clickable.

Is there a standard way to be able to quickly lookup where some term/identifier is defined (and the source code for it) when in a Coq file? Either in the CoqIDE or in emacs + ProofGeneral (I'm using CoqIDE, but I'd switch if emacs/ProofGeneral had this ability).

Or is the standard way to generate docs for every Coq project and dependency you use?

Upvotes: 8

Views: 866

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15404

There is a tool working on top of Proof General, called company-coq. It has the jump to definition feature bound to the M-. keyboard shortcut by default.

It can jump to the definition under cursor (even to the standard library) only if the module containing the definition is required with Require command or its variant.

Upvotes: 4

Jason Gross
Jason Gross

Reputation: 6128

If you highlight a term, and do Queries -> Locate, or you evaluate Locate some_identifier., you will get the full name of the constant. If you know where the dependencies are installed, this will tell you where to look for the identifier.

Edit: If you want the definition of the identifier, you can Print it. If you just want it's type, you can use About, or Check (which also accepts expressions, and not just identifiers).

Upvotes: 7

Related Questions