search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

Translate local notation with `(priority := high)` #162

Open gebner opened 2 years ago

gebner commented 2 years ago

This is closer to the Lean 3 semantics.

digama0 commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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).