Stream: Coq users

Topic: Notation levels


view this post on Zulip Shea Levy (Oct 13 2020 at 12:50):

How do you decide which level to define your notation at?

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 12:56):

The answer is long and not easy, so do you have some examples to scope discussion a bit? Just so that I start with the relevant issues.

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 12:57):

Also, do you already understand LL(1) parsing and the documented automatic left-factoring?

view this post on Zulip Enrico Tassi (Oct 13 2020 at 12:58):

You can also give a try to Print Grammar https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#coq:cmd.print-grammar and see where your new infix fits w.r.t. the existing ones.

view this post on Zulip Paolo Giarrusso (Oct 13 2020 at 12:59):

And how big is the target audience, and do they use libraries with similar notations, or even the same in other scopes? And do you want to get this right ahead of time, or prefer to change it later when you run into actual issues?

view this post on Zulip Shea Levy (Oct 13 2020 at 13:02):

Oof :grinning: Well, the example I'm looking at currently is a formalization of sequent calculus and the notation is x ⊢ y , I currently have an audience of one, and I'm happy to adjust later as long as it's not a massive non-mechanical change

view this post on Zulip Shea Levy (Oct 13 2020 at 13:03):

I have a stale grasp of LL(1) parsing and have read the whole syntax extensions section at various points, but not dug into the details lately.


Last updated: Jan 31 2023 at 14:03 UTC