The Coq mailing list

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

':>' is not a notation

Ah yes, you have me there.

On 1 August 2014 16:36, Cedric Auger <sedrikov AT gmail.com> wrote:

2014-08-01 6:59 GMT+02:00 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

As far as I know, ':>' is not a notation, but it is part of the grammar. In these conditions, I hardly see what Locate could do in this respect. At most, all that could be done, would be to add all tokens of the Coq parser in an extended index.
 

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

--
.../Sedrikov\...