Stream: Coq users

Topic: Using non-terminal in notations


view this post on Zulip Cyril Cohen (Nov 26 2020 at 13:50):

At some point, I thought this long awaited feature had been implemented, but I cannot find it in the doc. Is it wishful thinking?

view this post on Zulip Enrico Tassi (Nov 26 2020 at 13:52):

They are called "custom entries" (in the whole Coq sources, and "entry" is a "non terminal")

view this post on Zulip Enrico Tassi (Nov 26 2020 at 13:52):

don't ask me why

view this post on Zulip Cyril Cohen (Nov 26 2020 at 13:52):

thanks!


Last updated: Jan 29 2023 at 01:02 UTC