ambiguous interpretation at Data.List.Infix

Stream: mathlib4

[Henrik Böving]

Lean throws a tantrum on Data.List.Infix because basically all theorem statements are deemed to be ambiguous:

import Mathlib.Data.List.Basic

set_option pp.notation false in
set_option pp.explicit true in
example (xs : List Nat) : xs <+: xs := sorry

Here it throws the error:

ambiguous, possible interpretations
  @isPrefix Nat xs xs : Prop

  @isPrefix Nat xs xs : Prop

I don't see why it believes these are ambiguous? They look very much the same to me?

[Henrik Böving]

(deleted)

[Floris van Doorn]

did some notation get declared twice?

[Kevin Buzzard]

@[inherit_doc] infixl:50 " <+: " => isPrefix in Std.Data.List.Basic and infixl:50 " <+: " => isPrefix in Mathlib.Data.List.Defs

[Henrik Böving]

Yeah just saw it as well

[Henrik Böving]

so I guess I'll just delete the Mathlib line?

[Kevin Buzzard]

The other alternative is to just never use the notation, which appears to be what's going on right now ;-)

[Henrik Böving]

Given that basically all theorems in the file are stated with this notation I think I will avoid that :P

[Kevin Buzzard]

I'm surprised that Lean didn't complain when it ran into both definitions. Edit: maybe I'm not surprised.

[Kevin Buzzard]

notation " foo " => Nat
notation " foo " => Nat
notation " foo " => Int

works fine. I thought that we were somehow forced to "name" notation when we were overloading?

[Henrik Böving]

No lean does have the ability to figure out based on type inference what notation to use. So when you have multiple notations for the same thing it can actually start elaborating all of them and only if more than one (or none) suceed will it start to complain

[Henrik Böving]

I see that Data.List.Infix has some theorems about docs#list.init which is kind of like list.head but a little more toned down on errors, we don't have that function in Lean 4 core, what is our policy for this? Shall I just define it inline?

[Yaël Dillies]

list.init lives in init.data.list.basic, so you should define it in Mathlib.Init.Data.List.Basic.

[Henrik Böving]

Okay that file already got list.init ported by aligning it to dropLast. In that case do I just rename all of the theorems accordingly yes?

Furthermore there are a bunch of theorems about nthLe which is marked as deprecated in favor of List.get, shall I change those theorems as well or leave them be?

[Mario Carneiro]

the theorems about nthLe should be deprecated, not changed