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

chore: generalize List.get_mem #6095

Merged
merged 4 commits into from
Nov 19, 2024
Merged

chore: generalize List.get_mem #6095

merged 4 commits into from
Nov 19, 2024

Conversation

eric-wieser
Copy link
Contributor

This is syntactically more general than before, though up to eta expansion it make no difference.

@eric-wieser eric-wieser marked this pull request as ready for review November 15, 2024 22:44
@eric-wieser eric-wieser requested a review from digama0 as a code owner November 15, 2024 22:44
@kim-em kim-em enabled auto-merge November 18, 2024 03:42
@kim-em kim-em disabled auto-merge November 18, 2024 03:42
@kim-em kim-em added the awaiting-author Waiting for PR author to address issues label Nov 18, 2024
@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 Nov 18, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 18, 2024 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ecbaeff24b2cb36d5c218f4ed6c92d6d55524048 --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 21:06:07)
  • 💥 Mathlib branch lean-pr-testing-6095 build failed against this PR. (2024-11-19 05:56:45) View Log
  • 🟡 Mathlib branch lean-pr-testing-6095 build against this PR was cancelled. (2024-11-19 08:23:40) View Log
  • 💥 Mathlib branch lean-pr-testing-6095 build failed against this PR. (2024-11-19 08:32:12) View Log
  • ✅ Mathlib branch lean-pr-testing-6095 has successfully built against this PR. (2024-11-19 09:47:24) View Log

eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 18, 2024
@eric-wieser
chore: fix defeq abuse between List.get_mem and List.getElem_mem
1e0407b 
This will reduce the fallout of leanprover/lean4#6095.
@eric-wieser eric-wieser mentioned this pull request Nov 18, 2024
Closed
@eric-wieser
Copy link
Contributor Author

leanprover-community/mathlib4#19224 should halve the amount of fallout in mathlib

@kim-em kim-em removed the awaiting-author Waiting for PR author to address issues label Nov 19, 2024
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 19, 2024
@eric-wieser
chore: fix defeq abuse between List.get_mem and List.getElem_mem (#…
955e8f9 
…19224)

In all these places the goal state is about `getElem` not `List.get`.

This will reduce the fallout of leanprover/lean4#6095.
@eric-wieser @kim-em
chore: generalize List.get_mem
14112f7 
This is syntactically more general than before, though up to eta expansion it make no difference.
@eric-wieser @kim-em
Update Lemmas.lean
a813d39
@eric-wieser @kim-em
Update Attach.lean
a5e74f4
@eric-wieser @kim-em
Update RupAddResult.lean
5372af3
@kim-em
Copy link
Collaborator

kim-em commented Nov 19, 2024

(I rebased onto nightly-with-mathlib)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 19, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6095
a8815f0
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 19, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6095
7f8d4bd
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan 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 Nov 19, 2024
@kim-em kim-em mentioned this pull request Nov 19, 2024
Closed
@kim-em kim-em added this pull request to the merge queue Nov 19, 2024
Merged via the queue into leanprover:master with commit d6f8980 Nov 19, 2024
22 checks passed
TobiasLeichtfried pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 21, 2024
@eric-wieser @TobiasLeichtfried
chore: fix defeq abuse between List.get_mem and List.getElem_mem (#…
9e2db35 
…19224)

In all these places the goal state is about `getElem` not `List.get`.

This will reduce the fallout of leanprover/lean4#6095.
@kim-em kim-em added the changelog-library Library label Jan 4, 2025
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@eric-wieser @JovanGerb
chore: generalize List.get_mem (leanprover#6095)
6b87d29 
This is syntactically more general than before, though up to eta
expansion it make no difference.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

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

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

Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library 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.
3 participants
@eric-wieser @leanprover-community-bot @kim-em