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

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.

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

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.

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?

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

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