Translate local notation with (priority := high)

[gebner]

This is closer to the Lean 3 semantics.

[digama0]

Is it possible to predict when we need this? I would guess that in most cases it's not needed since even if there is an overlapping notation the local notation comes last. It's only if there is another (priority := high) global notation that this would make a difference AFAICT.

I really want to avoid adding "backward compatibility" flags on generated syntax by default, because the generated syntax should be as close as possible to the final "native-looking" result as possible. If we can't correctly make the determination of whether it is needed or not I would err on the side of nice looking results rather than technically correct results.

Alternatively, if we find that we almost always want local notations to be priority high, we should probably change the default in lean 4 core instead.

[gebner]

I think the Lean 4 default is the right one, I wouldn't change that.

I would guess that in most cases it's not needed since even if there is an overlapping notation the local notation comes last.

No, it's needed because otherwise you get a choice node. This can easily be ambiguous e.g. if you override +. We have a whole lot of local infixr ^ etc. in mathlib.

[digama0]

Oh yeah that's bad. It should be possible to write a function which determines if a syntax already exists, essentially by translating syntax term " + " term : term into $_:term + $_:term and then seeing if this parses. Synport keeps an up to date syntactic environment, so it should be fine to just do that in the current environment and if it looks like there is a duplicate, only then add the (priority := high).