protecting structure projections

Stream: mathlib4

[Jireh Loreaux]

How do I protect structure projections in Lean 4? I mean, I know that

structure Foo where
  protected bar : ℕ

works, but if I have a class Foo that extends Bar and Baz, how do I protect Foo.toBar and Foo.someBazField? It seems that attribute [protected] Foo.toBar doesn't work after the fact.

[Yaël Dillies]

Is protect_projs still a thing?

[Jireh Loreaux]

Doesn't seem to be.