module system and private defs

Stream: mathlib4

[Sébastien Gouëzel]

I'd like to understand a little bit better the module system. In #34499, I have a file with

def AddContent.supClosureFun := ...

def AddContent.supClosure : ... where
  toFun := AddContent.supClosureFun
  properties := ...

lemma AddContent.supClosure_apply : ...

The precise definition in AddContent.supClosureFun is an implementation detail, that is not useful nor relevant. Downstream, people should never have a need for the function AddContent.supClosureFun, and neither for the precise definition of AddContent.supClosure. The only property they should use is the lemma AddContent.supClosure_apply which says everything there is to know about it.

I'd like to make the definition AddContent.supClosureFun private, and also say that the implementation of AddContent.supClosure is private, while still making the definition and the lemma available in subsequent files. To me, this looks like a perfect situation for the module system, except that I don't know the right incantations. Could someone confirm that this is the kind of task where the module system shines, and how to do it?

[Aaron Liu]

try private def AddContent.supClosureFun := ... and @[no_expose] def AddContext.supClosure : ... where

[Aaron Liu]

private def makes the entire declaration not available to other files, and @[no_expose] def makes the contents of the declaration not available to other files

[Frédéric Dupuis]

I think @[no_expose] is the default, no? (At least if we don't put in the @[expose] public section that's in nearly every file currently.)

[Aaron Liu]

yeah, private and @[no_expose] it is the default

[Aaron Liu]

the relevant file has @[expose] public section at the top so you do have to @[no_expose] explicitly to override that

[Sébastien Gouëzel]

I've done that. Thanks!