chore: remove duplicate instances #8397
Merged
Conversation
This file contains hidden or 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
bf7bb12 to
756b044
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
May 19, 2025
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 19, 2025
|
kim-em
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
May 19, 2025
|
eric-wieser
reviewed
May 19, 2025
| @@ -161,8 +161,7 @@ This function does not reduce in the kernel. It is compiled to the C inequality | |||
| match a, b with | |||
| | ⟨a⟩, ⟨b⟩ => floatSpec.decLe a b | |||
|
|
|||
| instance floatDecLt (a b : Float) : Decidable (a < b) := Float.decLt a b | |||
| instance floatDecLe (a b : Float) : Decidable (a ≤ b) := Float.decLe a b | |||
| attribute [instance] Float.decLt Float.decLe | |||
There was a problem hiding this comment.
Can you inline the instance above?
jcommelin
pushed a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jun 4, 2025
* Update lean-toolchain for testing leanprover/lean4#8347 * fixes for leanprover/lean4#8347 * Update lean-toolchain for testing leanprover/lean4#8397 * deprecations for leanprover/lean4#8397 * chore: bump to nightly-2025-05-19 * chore: adaptations for nightly-2025-05-19 * Trigger CI for leanprover/lean4#8347 * Update the style linter to use LinterOptions * Fix test * chore: adaptations for nightly-2025-05-19 (#25017) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> * chore: bump to nightly-2025-05-20 * Merge master into nightly-testing * feat: a `grind` test case (#25037) Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test. Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.) * lake update * fixes * fixes * fixes * fixes * fix * fixes * fixes * shake --update * chore: bump to nightly-2025-05-21 * Update lean-toolchain for testing leanprover/lean4#7352 * lake update * Trigger CI for leanprover/lean4#7352 * chore: adaptations for nightly-2025-05-21 * chore: adaptations for nightly-2025-05-21 (#25079) Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> * chore: adaptations for nightly-2025-05-21 * fix for leanprover/lean4#7352 * remove unneeded List.ofFn_succ from simp sets * Merge master into nightly-testing * Merge master into nightly-testing * Revert "fix for leanprover/lean4#7352" This reverts commit 38ca408. * chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098) Follows on from leanprover/lean4#7352. This also deprecates: * `id.mk`, which looks like a porting error * `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere. * chore: bump to nightly-2025-05-22 * update batteries * chore: bump to nightly-2025-05-23 * Update lean-toolchain for testing leanprover/lean4#8449 * chore: adaptations for nightly-2025-05-22 (#25110) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> * remove now upstreamed `clear_value` * Update lean-toolchain for testing leanprover/lean4#8457 * chore: update tests for `Format` bug fix * Trigger CI for leanprover/lean4#8457 * lake update * lake update * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-24 * fix * chore: adaptations for nightly-2025-05-24 (#25147) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: github-actions <github-actions@github.com> * chore: adaptations for nightly-2025-05-24 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8470 * chore: bump to nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 * chore: adaptations for nightly-2025-05-25 (#25184) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> * unsimp `List.getElem?_length` This is solved using `getElem?_neg` now. * chore: adaptations for nightly-2025-05-25 * Trigger CI for leanprover/lean4#8470 * chore: bump to nightly-2025-05-26 * lake update * deprecations * Trigger CI for leanprover/lean4#8449 * Merge master into nightly-testing * chore: bump to nightly-2025-05-27 * chore: adaptations for nightly-2025-05-27 * Update lean-toolchain for testing leanprover/lean4#8504 * chore: bump to nightly-2025-05-28 * chore: adaptations for nightly-2025-05-27 (#25234) Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * fix * fix merge * fix merge again * deprecations * deprecations * fix Archive * comment out test * Fix and re-enable directory dependency lint test. * chore: bump to nightly-2025-05-29 * Use the formatting from the master branch. (Seems to have been a merge that went wrong.) * lake update * chore: adaptations for nightly-2025-05-28 (#25295) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> * fix * Trigger CI for leanprover/lean4#8337 * fixes * Merge master into nightly-testing * chore: bump to nightly-2025-05-30 * chore: adaptations for nightly-2025-05-29 (#25306) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> * chore: bump to nightly-2025-05-31 * chore: bump to nightly-2025-06-01 * fix Archive * chore: adaptations for nightly-2025-06-01 (#25355) Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> * chore: bump to nightly-2025-06-02 * chore: adaptations for nightly-2025-06-02 (#25360) Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: github-actions <github-actions@github.com> * Update lean-toolchain for testing leanprover/lean4#8584 * chore: adaptations for nightly-2025-06-02 * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * chore: bump to nightly-2025-06-04 * bump toolchain --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
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.
This PR cleans up many duplicate instances (or, in some cases, needlessly duplicated
def X := ...; instance Y := X).