Skip to content

fix: fun_induction to generalize like induction does#7127

Merged
nomeata merged 5 commits intomasterfrom
joachim/fun_induction_generalize
Feb 18, 2025
Merged

fix: fun_induction to generalize like induction does#7127
nomeata merged 5 commits intomasterfrom
joachim/fun_induction_generalize

Conversation

@nomeata
Copy link
Copy Markdown
Collaborator

@nomeata nomeata commented Feb 18, 2025 •
edited
Loading

This PR follows up on #7103 which changes the generaliziation behavior of induction, to keep fun_induction in sync. Also fixes a Syntax indexing off-by-one error.

@nomeata
fix: fun_induction to generalize like induction does
a89f9dd 
This PR follows up on #7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction`  in sync.
@nomeata nomeata added the changelog-language Language features and metaprograms label Feb 18, 2025
@nomeata nomeata requested a review from kmill February 18, 2025 09:02
@nomeata nomeata requested a review from kim-em as a code owner February 18, 2025 09:02
@nomeata nomeata marked this pull request as draft February 18, 2025 09:16
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 18, 2025 09:24 Inactive
@nomeata nomeata marked this pull request as ready for review February 18, 2025 09:37
@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 Feb 18, 2025
@ghost
Copy link
Copy Markdown

ghost commented Feb 18, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d9e7ded5afce0b321055439024374d7ec00805be --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-18 10:07:14)

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc February 18, 2025 10:19 Inactive
@nomeata nomeata added this pull request to the merge queue Feb 18, 2025
Merged via the queue into master with commit f3baff8 Feb 18, 2025
13 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 24, 2025
@nomeata @luisacicolini
fix: fun_induction to generalize like induction does (leanprover#7127)
c12bf0b 
This PR follows up on leanprover#7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction` in sync. Also fixes a `Syntax`
indexing off-by-one error.
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Feb 25, 2025
@nomeata @luisacicolini
fix: fun_induction to generalize like induction does (leanprover#7127)
755ae57 
This PR follows up on leanprover#7103 which changes the generaliziation behavior
of `induction`, to keep `fun_induction` in sync. Also fixes a `Syntax`
indexing off-by-one error.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kmill kmill Awaiting requested review from kmill

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

changelog-language Language features and metaprograms 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.

1 participant

@nomeata