Commit 2026-09-03 17:31 53c9b00b

feat: linter for internal constructors (#42883) This PR lints against using internal constructors during elaboration (i.e. those with a name component that starts with _, e.g. _mkInternal). This allows us to preserve defeq properties (such as in category theory) and avoid set_option backward.privateInPublic false while still preventing uses downstream through ⟨_⟩. This linter does not fire in the file in which the internal constructor is defined.