Modules and init

Stream: lean4

[François G. Dorais]

I'm still to fully understand the module system, so this may be a basic question.

This mwe doesn't work if I don't make myInt.init public.

module

public protected unsafe def myInt.init : IO Int := pure 42

@[init myInt.init] public def myInt : Int := default

Obviously, myInt.init is not meant to be used outside this particular module. It is also not useful to make it public in serious use cases.

Is this a bug or is there a deeper reason why I need to make init code public?

[Sebastian Ullrich]

No deeper reason, but is there a reason you're not using initialize?

[François G. Dorais]

Mostly cosmetic, I think. For my use cases, the initialization code is about 100 lines with a couple of where definitions. Using @[init] seems more ergonomic than initialize.

Is there a benefit to using initialize that I'm not seeing?