deprecated and dot notation

Stream: lean4

[Yury G. Kudryashov]

Here is an #mwe

structure A where
  n : Nat
  n_eq : n = 42

namespace A

@[deprecated n_eq] theorem n_eq' (x : A) : x.n = 42 := x.n_eq

example (x : A) : x.n = 42 := x.n_eq' -- no warning
example (x : A) : x.n = 42 := n_eq' x -- `A.n_eq'` has been deprecated

end A

[Yury G. Kudryashov]

This means that one can use deprecated theorems without getting warning. This happened in Mathlib with lemmas like RingHom.map_prod.

[Eric Wieser]

There is an open issue about this already

[Yury G. Kudryashov]

I'm sorry for not reading existing issues first.

[Eric Wieser]

lean4#3270