irreducible_def = public non-exposed def ?

Stream: mathlib4

[Jz Pan]

With the newly introduced module system, seems that the irreducible_def (defined in mathlib, but not vanilla Lean) is equivalent to the public non-exposed def in module system. Is that true? (Of course irreducible_def also works for non-module file.)

[Aaron Liu]

Well with non-exposed defs their contents are still exposed to the private scope

[Jovan Gerbscheid]

Yes, I think we should eventually get rid of all uses of irreducible_def in favour of not exposing the body.

The problem for now is that other projects that depend on mathlib may not have switched to the module system yet. So then the unexposed bodies of definitions are going to be exposed anyways there.

[Jz Pan]

Jovan Gerbscheid said:

The problem for now is that other projects that depend on mathlib may not have switched to the module system yet. So then the unexposed bodies of definitions are going to be exposed anyways there.

I haven't checked the behavior of a non-module file importing a module file. Will it also import the private section of a file?

[Jovan Gerbscheid]

Yes, a non-module always imports everything