compilation success depends on theorem name!

Stream: lean4

[Kevin Buzzard]

variable {C : Type}
variable {D : Type}

def Additive (α : Type) := α

structure Func (C D : Type) where

class Func.Additive {C : Type} {D : Type} (F : Func C D) : Prop where

theorem Func.bar (F : Func C D) [Additive F] : 2+2=4 := rfl -- works
theorem baz (F : Func C D) [Additive F] : 2+2=4 := rfl -- error!

Is this expected? In mathlib there is CategoryTheory.Functor.Additive and Additive, and this just bit me. The Additive which is picked up by Additive F depends on the name of the theorem being defined!

[Gabriel Ebner]

Yes, this is intentional (iirc Reid campaigned for it).

def Func.bar := 42
-- is the same as:
namespace Func
def bar := 42
end Func

and in particular all names from Func are in scope.

[James Gallicchio]

maybe the non-toplevel additive should be protected?

[Kevin Buzzard]

In my use case, F.Additive works fine BTW