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: Sep 23 2023 at 08:01 UTC