Is it possible to find notations associated to a keyword? Eg if I forget how to write the infix notation for equality, how do I find "_ = _" ?
I don't know any other way than to write eq u v
and have it printed by Coq to u = v
. But it wouldn't fork for parse only
notations.
You can do Print Scopes.
and then search for your constant in the output
Last updated: Oct 13 2024 at 01:02 UTC