feat: swap arguments to Membership.mem
#5020
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 13, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 13, 2024
leanprover-community-mathlib4-bot
added
breaks-mathlib
|
Mathlib CI status (docs):
|
|
I should have clean CI for the PR branch of mathlib and all but one core test passing. I will try to fix that later tonight and highlight the less-than-desirable changes. |
leanprover-community-mathlib4-bot
added
builds-mathlib
|
awaiting-review |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 16, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Aug 16, 2024
|
@TwoFX and @semorrison I attempted to apply the label for awaiting review but it failed. There is now a working branch of mathlib. I created leanprover-community/mathlib4#15870 to, at the moment, provide an interface to highlight anything surprising. |
kim-em
force-pushed
the
mrb/mem_swap
branch
2 times, most recently
from
af06c79 to
88ce999
Compare
kim-em
reviewed
Aug 23, 2024
src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
Outdated
Show resolved
Hide resolved
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 23, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 23, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Aug 24, 2024
leanprover-community-mathlib4-bot
added
breaks-mathlib
leanprover-community-mathlib4-bot
added
builds-mathlib
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 5, 2024
Currently we use `Set.inclusion` to construct functions between `Opens`. This is a form of defeq abuse which is exposed by leanprover/lean4#5020. In this PR, we introduce `Opens.inclusion` and replace uses of `Set.inclusion` with it to avoid passing through a coercion to `Set`. Since there is a version, not analogous to `Set.inclusion`, squatting on this name we rename it to `Opens.inclusion'`. Co-authored-by: Matthew Robert Ballard <[email protected]>
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 6, 2024
We make miscellaneous changes to either remove or clarify `adaptation_notes` coming from leanprover/lean4#5020. Co-authored-by: Kim Morrison <[email protected]>
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 9, 2024
Currently we use `Set.inclusion` to construct functions between `Opens`. This is a form of defeq abuse which is exposed by leanprover/lean4#5020. In this PR, we introduce `Opens.inclusion` and replace uses of `Set.inclusion` with it to avoid passing through a coercion to `Set`. Since there is a version, not analogous to `Set.inclusion`, squatting on this name we rename it to `Opens.inclusion'`. Co-authored-by: Matthew Robert Ballard <[email protected]>
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 9, 2024
We make miscellaneous changes to either remove or clarify `adaptation_notes` coming from leanprover/lean4#5020. Co-authored-by: Kim Morrison <[email protected]>
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 9, 2024
Currently we use `Set.inclusion` to construct functions between `Opens`. This is a form of defeq abuse which is exposed by leanprover/lean4#5020. In this PR, we introduce `Opens.inclusion` and replace uses of `Set.inclusion` with it to avoid passing through a coercion to `Set`. Since there is a version, not analogous to `Set.inclusion`, squatting on this name we rename it to `Opens.inclusion'`. Co-authored-by: Matthew Robert Ballard <[email protected]>
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 9, 2024
We make miscellaneous changes to either remove or clarify `adaptation_notes` coming from leanprover/lean4#5020. Co-authored-by: Kim Morrison <[email protected]>
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 12, 2024
Currently we use `Set.inclusion` to construct functions between `Opens`. This is a form of defeq abuse which is exposed by leanprover/lean4#5020. In this PR, we introduce `Opens.inclusion` and replace uses of `Set.inclusion` with it to avoid passing through a coercion to `Set`. Since there is a version, not analogous to `Set.inclusion`, squatting on this name we rename it to `Opens.inclusion'`. Co-authored-by: Matthew Robert Ballard <[email protected]>
bjoernkjoshanssen
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 12, 2024
We make miscellaneous changes to either remove or clarify `adaptation_notes` coming from leanprover/lean4#5020. Co-authored-by: Kim Morrison <[email protected]>
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 24, 2024
…dule` to get a type (#16509) We add ```lean instance (priority := high) coeSort : CoeSort (LieSubmodule R L M) (Type w) where coe N := { x : M // x ∈ N } ``` to avoid the coercion to a `Sort` being `{ x : M // x ∈ N.toSubmodule }` and instead be `N` itself. This allows removal of all `adapation_note`s from leanprover/lean4#5020. Ultimately the API here should be expanded and `Coe (LieSubmodule R L M) (Submodule R M)` should be minimized or removed to avoid forcing Lean to unify `LieSubmodule` and `Submodule` unnecessarily. Co-authored-by: Matthew Robert Ballard <[email protected]>
mathlib-bors bot
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Sep 27, 2024
This was broken by leanprover/lean4#5020
fbarroero
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Oct 2, 2024
This was broken by leanprover/lean4#5020
nahcnuj
added a commit
to nahcnuj/hello-type-system
that referenced
this pull request
Oct 10, 2024
The parameters to Membership.mem have been swapped, which affects all Membership instances. leanprover/lean4#5020
3 tasks
Merged
3 tasks
JovanGerb
pushed a commit
to JovanGerb/lean4
that referenced
this pull request
Jan 21, 2025
This PR fixes `simp only [· ∈ ·]` after leanprover#5020. Fixes leanprover#5905
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We swap the arguments for
Membership.memso that when proceeded by aSetLikecoercion, as is often the case in Mathlib, the resulting expression is recognized as eta expanded and reduce for many computations. The most beneficial outcome is that the discrimination tree keys for instances and simp lemmas concerning subsets become more robust resulting in more efficient searches.Closes
RFC#4932