Skip to content

fix: allow arbitrary sorts in structural recursion over reflexive inductive types #7639

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

fix: allow arbitrary sorts in structural recursion over reflexive inductive types #7639

wants to merge 1 commit into from

Conversation

cppio
Copy link
Contributor

@cppio cppio commented Mar 22, 2025

This PR changes the generated below and brecOn implementations for reflexive inductive types to support motives in Sort u rather than Type u.

Closes #7638

@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 Mar 22, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-03-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-22 22:11:29)

@cppio
Copy link
Contributor Author

cppio commented Mar 22, 2025

changelog-language

@github-actions github-actions bot added the changelog-language Language features, tactics, and metaprograms label Mar 22, 2025
@cppio cppio marked this pull request as ready for review March 22, 2025 22:29
@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label Mar 25, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms P-low We are not planning to work on this issue toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Cannot eliminate reflexive inductive type into arbitrary sort
3 participants
@cppio @leanprover-community-bot @leanprover-bot