Shea Levy (Oct 13 2020 at 12:50): Shea Levy (Oct 13 2020 at 12:50):How do you decide which level to define your notation at?
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.
Paolo Giarrusso (Oct 13 2020 at 12:57):Also, do you already understand LL(1) parsing and the documented automatic left-factoring?
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.
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?
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
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: Sep 23 2023 at 15:01 UTC