Skip to content
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

feat: use reserved name infrastructure for functional induction #3776

Merged
merged 2 commits into from
Mar 26, 2024
Merged

feat: use reserved name infrastructure for functional induction #3776

merged 2 commits into from
Mar 26, 2024

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Mar 26, 2024

no need to enter derive_functional_induction anymore.

(Will remove the support for derive_functional_induction after the
next stage0 update, since we are already using it in Init.)

@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 26, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Mar 26, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0c6c5d226883980cfe986886681e68e9924f2bd --onto 80d2455b6401acf6b0d107388b814c175e64c0d3. (2024-03-26 14:25:07)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 466ef74ccc024e334e9c78d9e008d3f7612f9ccf --onto 4c0106d757d4d6d3b7f3903611ce22100d539d2a. (2024-03-26 16:05:23)

@nomeata
feat: use reserved name infrastructure for functional induction
4368789 
no need to enter `derive_functional_induction` anymore.

(Will remove the support for `derive_functional_induction` after the
next stage0 update, since we are already using it in Init.)
@nomeata nomeata force-pushed the joachim/funind-reserved branch from 34798ea to 4368789 Compare March 26, 2024 15:46
@nomeata nomeata changed the base branch from joachim/funind-structural to master March 26, 2024 15:46
@nomeata nomeata marked this pull request as ready for review March 26, 2024 15:47
@nomeata nomeata closed this Mar 26, 2024
@nomeata nomeata reopened this Mar 26, 2024
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 26, 2024 21:37 Inactive
@nomeata nomeata added this pull request to the merge queue Mar 26, 2024
Merged via the queue into master with commit ab318dd Mar 26, 2024
11 checks passed
nomeata added a commit that referenced this pull request Mar 27, 2024
@nomeata
fix: remove derive_functional_induction
90f86a4 
this follows up on #3776 and the subsequent stage0 update, now relying
on the reserved name for the induction principles.
@nomeata nomeata mentioned this pull request Mar 27, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 27, 2024
@nomeata
fix: remove derive_functional_induction (#3788)
c857d08 
this follows up on #3776 and the subsequent stage0 update, now relying
on the reserved name for the induction principles.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

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

Assignees
No one assigned
Labels
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.
2 participants
@nomeata @leanprover-community-mathlib4-bot