The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014-07-31 9:30 GMT+02:00 <michael.soegtrop AT intel.com>:

Dear Coq users,

is there a good way to look up the definition of a notation or to unfold
notations in a goal or hypothesis? In proofs one typically has to use the
"real names", but I tend to forget these and the best way I found to look up
the definition of a notation is grep, which is not so convenient.

Best regards,

Michael

You can deactivate notations (in the menus of the IDE), read your hypothesis, and reactivate them.
That would not qualify as a "good way" since it will unfold *all* the notations and not only the one you want.
Still, it seems better than using grep (although the purpose is slightly different as with my solution you need to have an hypothesis under focus in your IDE, and you have the advantage of not manually apply the Notation, while in the grep solution, you get the definition and do not require to have an hypothesis under focus, which can be helpful if you want to write a term or just to focus on the Notation itself, but you have to manually apply the Notation to your context if you have one).

I think there is something that does what your grep tool does. That must be in the reference manual (Locate).

http://coq.inria.fr/refman/Reference-Manual008.html#hevea_command135


By the way, the documentation has problems with the '%' character as seen in:

http://coq.inria.fr/refman/Reference-Manual008.html#hevea_command132

--
.../Sedrikov\...