Skip to content

fix: adjust name mangling in kernel's nested inductive type processing - #14846

Draft
kmill wants to merge 1 commit into
masterfrom
kmill_fix_10789
Draft

fix: adjust name mangling in kernel's nested inductive type processing#14846
kmill wants to merge 1 commit into
masterfrom
kmill_fix_10789

Conversation

@kmill

@kmill kmill commented Aug 19, 2026

Copy link
Copy Markdown
Collaborator

This PR fixes an issue where the kernel would not accept nested inductive types where the type being nested through was public with a private constructor. The kernel assumed that the name of the inductive type was a prefix of each constructor. Now the kernel uses a simpler procedure where the auxiliary type's name is prepended to constructor names, rather than replacing a prefix. Note that a consequence to this is that auxiliary recursors have non-atomic minor premise names (which was already the case for private constructors).

With @berberman

Closes #10789

@kmill kmill added the changelog-language Language features and metaprograms label Aug 19, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 19, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 19, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-19 18:54:50)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase de315cfb508e9e7bc5e744546fbc329331a64567 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 17:02:22)
  • ✅ Mathlib branch lean-pr-testing-14846 has successfully built against this PR. (2026-08-25 22:53:45) View Log

@leanprover-bot

leanprover-bot commented Aug 19, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-19 18:54:52)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase de315cfb508e9e7bc5e744546fbc329331a64567 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-20 17:02:24)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-25 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-25 21:57:17)

This PR fixes an issue where the kernel would not accept nested inductive types where the type being nested through was public with a private constructor. The kernel assumed that the name of the inductive type was a prefix of each constructor. Now the kernel uses a simpler procedure where the auxiliary type's name is prepended to constructor names, rather than replacing a prefix. Note that a consequence to this is that auxiliary recursors have non-atomic minor premise names (which was already the case for private constructors).

With @berberman
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Aug 25, 2026
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Aug 25, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Cannot recurse through type with a private constructor

2 participants