Commit 2026-05-07 10:00 45e1dd8f

refactor: don't expose definitions of immersions (#39002) Instead of using an irreducible_def, make it an unexposed definition. This has the same effect in other modules, but leads to much shorter code as we can remove all rw [foo_def] for the immersion definitions. It also allows removing the @[expose] section from the file (which is nice). There is a small downside: in downstream projects not using the module system, the definition of immersions will be unfolded now. At this point, this is a mostly hypothetical risk (and weighs lower than the real benefits of this change). The discussion leading to this change did not have substantial evidence either. Inspired by the discussion in #35122.