Zulip Chat Archive

Stream: mathlib4

Topic: unsupported: ambiguous notation

David Renshaw (Feb 28 2023 at 13:54):

When porting what are we supposed to do about the comment

unsupported: ambiguous notation

?

David Renshaw (Feb 28 2023 at 13:55):

e.g. https://github.com/leanprover-community/mathlib3port/blob/208d1f403d591be4023eb8d5b3989eb8cd3e1a3b/Mathbin/Data/Nat/Digits.lean#L62

David Renshaw (Feb 28 2023 at 13:56):

My inclination is to delete these comments, but I see that some of them have landed on master: https://github.com/leanprover-community/mathlib4/blob/35dd23d0c6eb5921c1629ffb476573dc8d73b95d/Mathlib/Data/Set/Lattice.lean#L1347

Kyle Miller (Feb 28 2023 at 14:06):

For the first one, I think it's just reporting that :: could mean a number of things -- it's overloaded in mathlib.

For the second, it should be a similar reason, but this time for ×ˢ which is also overloaded.

David Renshaw (Feb 28 2023 at 14:09):

My feeling about these is that they are warnings to the person doing the porting that the mathport output might not be accurate. If we get the resulting code to work, then it seems to me that the warning is no longer serving a purpose.

David Renshaw (Feb 28 2023 at 14:10):

Does that sound right?

Reid Barton (Feb 28 2023 at 14:13):

How does overloaded notation work in Lean 4? Is it just "most recent one wins"?

David Renshaw (Feb 28 2023 at 14:14):

FWIW, here's the relevant code in mathport: https://github.com/leanprover-community/mathport/blob/e2b9ccc6caac42ba52192389ea954f4961f60f7c/Mathport/Syntax/Translate/Expr.lean#L174-L177

Reid Barton (Feb 28 2023 at 14:17):

I agree that what the message is warning about it is not a problem locally if you get the code to compile, but maybe it indicates an issue with the notation itself?

David Renshaw (Feb 28 2023 at 14:19):

some other instances of the :: notation:
https://github.com/leanprover-community/mathlib4/blob/35dd23d0c6eb5921c1629ffb476573dc8d73b95d/Mathlib/Data/Sym/Basic.lean#L246
https://github.com/leanprover-community/mathlib4/blob/35dd23d0c6eb5921c1629ffb476573dc8d73b95d/Mathlib/Data/Stream/Defs.lean#L39

David Renshaw (Feb 28 2023 at 14:19):

both of those are scoped

David Renshaw (Feb 28 2023 at 14:20):

also scoped: https://github.com/leanprover-community/mathlib4/blob/35dd23d0c6eb5921c1629ffb476573dc8d73b95d/Mathlib/Data/Num/Bitwise.lean#L238

Gabriel Ebner (Feb 28 2023 at 18:57):

The message is meant to say "unsupported [by mathport]: ambiguous notation".

Gabriel Ebner (Feb 28 2023 at 18:58):

Lean 4 does support ambiguous notation, but it causes a few more issues than in Lean 3.

Gabriel Ebner (Feb 28 2023 at 18:58):

For example, overloading :: breaks pattern matching iirc.

Gabriel Ebner (Feb 28 2023 at 18:58):

So I'd make all overloads scoped.

Gabriel Ebner (Feb 28 2023 at 18:59):

lean4#2050

David Renshaw (Feb 28 2023 at 19:08):

I removed the warnings from the PR in question: https://github.com/leanprover-community/mathlib4/pull/2300/commits/e868c073bb7188aefe6e7c922a3002d435fa1085

Last updated: Dec 20 2023 at 11:08 UTC