Julien Cretin
Julien Cretin
> associativity in notations is handled by directly sending the explicit level or NEXT on the right to the grammar Thanks! Indeed this matters in general. However I believe for...
> if you can test [proux01@4fdb719](https://github.com/proux01/rocq/commit/4fdb7190fb66528807d2e2a35f64dd11fcb8af67) and confirm it seems to do what you expect, that would be great Nice! You've fixed it. I've tested using the `check.sh` script in...
I should be able to attend.
We have `=` non-assoc at 70, `||` left-assoc at 50, `&&` left-assoc at 40, and `~~` right-assoc at 35. So it should indeed work (and is unaffected by the proposed...
The problem is still present at commit 9a872fe98cbf20a688ff35165f7f6a1b3f5b8380 (version 20250625.922), although #271 sounds like it should fix something similar.
We can now see from the levels that `;` is left-associative and `+` is right-associative:
I've edited the description. Not sure it's worth a log entry.
> They are included in the reference manual when the level is not empty. Look at the grammar for `term` or, above, `ltac_expr`. Can you provide a link? I don't...
> https://rocq-prover.org/doc/V9.1.0/refman/language/core/basic.html#grammar-token-term Thanks! I misread the "not empty" as "empty" and only searched for exact "foo4 := foo3" patterns... :sweat_smile: So indeed, the refman already takes the approach of elaborating...
> It should be done in English in one place in the manual, not in the grammar syntax. I would also prefer this. > I believe the current code includes...