Deprecated & namespace

Stream: mathlib4

[Andrew Yang]

In the following example, lean marks foo deprecated despite it is using the non-deprecated Foo.foo.

theorem Foo.foo : True := trivial

@[deprecated] def Bar.foo : Nat := 3

open Foo Bar

example : True := foo

[Damiano Testa]

Is https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Misfiring.20deprecation related?

[Kim Morrison]

Related to, but not exactly, lean#2132.

Would you mind opening an issue? (Perhaps link to lean#2132 in it.)

[Andrew Yang]

Ah didn't see that stream when searching. I opened #4636.

[Damiano Testa]

lean#4636?