Skip to content

feat: forall lemmas#12945

Merged
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:logic-simp-lemmas
Mar 17, 2026
Merged

feat: forall lemmas#12945
TwoFX merged 2 commits intoleanprover:masterfrom
TwoFX:logic-simp-lemmas

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Mar 17, 2026

This PR adds a few forall lemmas to the simp set.

@TwoFX TwoFX added the changelog-library Library label Mar 17, 2026
@TwoFX TwoFX requested a review from kim-em as a code owner March 17, 2026 12:43
@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 17, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 17, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-17 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-03-17 13:32:58)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 17, 2026
Update lean-toolchain for testing leanprover/lean4#12945
1d89757
@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 Mar 17, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 17, 2026
Update lean-toolchain for testing leanprover/lean4#12945
d28e8e4
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 17, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 17, 2026

Mathlib CI status (docs):

@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 17, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 17, 2026

Mathlib CI status (docs):

@TwoFX TwoFX added this pull request to the merge queue Mar 17, 2026
Merged via the queue into leanprover:master with commit 5f5a450 Mar 17, 2026
40 checks passed
@TwoFX TwoFX mentioned this pull request Mar 19, 2026
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 19, 2026
@TwoFX
perf: remove simp annotations (#12977)
a045a7c 
This PR removes most of the `simp` annotations added in #12945, to
mitigate the performance impact. The lemmas remain.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

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

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library 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

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@TwoFX @leanprover-bot