Stream: Coq users

Topic: Finding notations

view this post on Zulip Philipp G. Haselwarter (Jan 19 2021 at 21:24):

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 "_ = _" ?

view this post on Zulip Théo Winterhalter (Jan 19 2021 at 21:25):

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.

view this post on Zulip Jason Gross (Jan 23 2021 at 02:08):

You can do Print Scopes. and then search for your constant in the output

Last updated: Jun 14 2024 at 19:02 UTC