digama0
commented
1 year ago Yes, there is special handling for the <;> associativity change which needs to be removed. (I'm on leave right now, I will get back to this on monday.)
We should not need to rewrite a <;> (b <;> c) to (a <;> b) <;> c because ; is left associative in lean 3 to begin with. The only reason this should appear is if the original said a; (b; c) -- which you can't even write because () doesn't work like that in lean 3.
Oooh, this bump results in lots of "format: uncaught backtracking exception" errors. All of them seem to involve
<;>. @digama0 Any ideas what that could be?We should also rewrite
a <;> (b <;> c)into(a <;> b) <;> c. (I'm not even sure if we can right that as a single syntax matcher.)