8678c99b76
Previously, `elabInitialize` only checked for explicit `private` when deciding whether to mangle `fullId`, ignoring the `module` system's default-private semantics. It also overrode the user's visibility for the generated `initFn` via `visibility.ofBool`. Now, `elabInitialize` uses `elabVisibility` + `isInferredPublic` to correctly handle all visibility contexts. The generated `initFn` inherits the user's visibility rather than being forced public. Also factors out `elabVisibility` from `elabModifiers` for reuse.
27 lines
696 B
Text
27 lines
696 B
Text
module
|
|
|
|
/-!
|
|
`builtin_initialize` and `initialize` in a `module` without `private`/`public` should work, even
|
|
when the type references a non-public declaration.
|
|
-/
|
|
|
|
structure MyState where
|
|
value : Nat := 0
|
|
deriving Inhabited
|
|
|
|
builtin_initialize myState : IO.Ref MyState ← IO.mkRef {}
|
|
initialize myState' : IO.Ref MyState ← IO.mkRef {}
|
|
|
|
builtin_initialize
|
|
myState.modify fun s => { s with value := s.value + 1 }
|
|
|
|
-- Exercise match auxiliary generation inside `initialize` (reproducer for Batteries issue)
|
|
initialize myRef : IO.Ref Nat ← do
|
|
let x : Nat ⊕ Nat := .inl 42
|
|
let v := match x with
|
|
| .inl n => n
|
|
| .inr n => n + 1
|
|
IO.mkRef v
|
|
|
|
initialize
|
|
myRef.modify (· + 1)
|