protected private

Stream: lean4

[Eric Wieser]

Is it possible to combine the protected and private modifiers? In the following example, open foo exposes the private definition, presumably because it is not protected:

private def foo.bar := 1
protected def foo.baz := 1

open foo

#check bar -- works, but I want it to fail
#check baz -- fails, as intended

Is it possible to make a definition simultaneously private and protected?

[Alex J. Best]

This seems to only happen when the check lines are in the same file as the namespace, and private really shouldn't behave in this way normally