The Coq mailing list

[Christopher Ernest Sally <christopherernestsally AT gmail.com>]

Hmm, not denying Locate's usefulness but doesn't Locate only print out where is symbol is used (which I grant, often does give you what you need)? for example, the other day I wanted to know what ":>" was. Locate ":>". gave

Notation            Scope    
"x = y :> A" := eq x y         : type_scope
                      (default interpretation)
"x <> y  :> T" := not (eq x y) : type_scope
                      (default interpretation)

which didn't really help (I saw :> in the context of record coercions) and I then had to look it up the "normal" way (which for me is grep-ing the pdf manual).

Best

Chris

On 31 July 2014 15:42, Pierre-Evariste Dagand <pedagand AT gmail.com> wrote:

> is there a good way to look up the definition of a notation or to unfold
> notations in a goal or hypothesis?

"Locate" is your friend:
http://coq.inria.fr/refman/Reference-Manual014.html#hevea_command266


Cheers,

--
Pierre-Evariste