The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

I know how to use:

>>> Locate "_ /\ _".

I get back a result of:

>>> A /\ B = and A B

However, this is not sufficient. Is there a way to get back associativity and precedence level as well?

(In particular, I need to build a Notation that "mirrors" Coq Props, things like

/\ ==> e/\

\/ ==> e\/

-> ==> e->

and I would prefer that the two notations, modulo the objects they represent, operate on the same way.)

Thanks!