Sebastian Ullrich 8678c99b76 fix: respect module visibility in initialize/builtin_initialize ... 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.		2026-04-10 15:08:43 +02:00
..
commands	chore: add safety notes to release command (#13225)	2026-04-01 05:01:00 +00:00
skills	chore: fix profiler shebang and add profiling skill (#12519)	2026-03-01 07:09:33 +00:00
CLAUDE.md	fix: respect module visibility in initialize/builtin_initialize	2026-04-10 15:08:43 +02:00
settings.json	chore: enable leanprover/skills plugin for Claude Code (#12609)	2026-02-20 12:35:32 +00:00