Axioms don't respect private

Stream: general

[Wojciech Nawrocki]

Is this intended behaviour or a bug? From the reference: "bear the private modifier [..] An alias is generated at the point where the declaration is made and it survives until the namespace is closed, or to the end of the file if the declaration is at the top level."

namespace foo
private axiom bar: false
private def baz: ℕ := 0
end foo

#check foo.baz -- unknown identifier 'foo.baz'

#check foo.bar -- foo.bar : false
#print axioms -- foo.bar is here

[Chris Hughes]

I think it's the right behaviour, otherwise I could sneak extra axioms into my theorems and no one would know.

[Chris Hughes]

I think it's the right behaviour, otherwise I could sneak extra axioms into my theorems and no one would know.

[Wojciech Nawrocki]

If foo.bar was inaccessible outside foo, it could only be used by declarations in foo, but the usual axiom propagation mechanism through transitive dependency (a declaration depends on foo.bar if it uses another decl. that depends on foo.bar) could still work with the dependency chain always terminating at something in foo, so that sneaking in axioms wouldn't be possible. I guess maybe the issue is that it would be difficult for the propagation to refer to a private name.