Skip to content

[Merged by Bors] - chore(Order/Hom/Basic): fix EquivLike OrderIso instance diamond#38559

Closed
SnirBroshi wants to merge 2 commits intoleanprover-community:masterfrom
SnirBroshi:feature/order/delete-order-iso-equiv-like
Closed

[Merged by Bors] - chore(Order/Hom/Basic): fix EquivLike OrderIso instance diamond#38559
SnirBroshi wants to merge 2 commits intoleanprover-community:masterfrom
SnirBroshi:feature/order/delete-order-iso-equiv-like

Conversation

@SnirBroshi
Copy link
Copy Markdown
Collaborator

@SnirBroshi SnirBroshi commented Apr 26, 2026 •
edited
Loading

OrderIso is an abbrev for RelIso which already has an EquivLike instance.
Removing it creates issues with to_dual, so instead we make it defeq to the RelIso instance using inferInstance.

Zulip

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 26, 2026 •
edited
Loading

PR summary 10a055a908

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-order Order theory label Apr 26, 2026
@b-mehta b-mehta added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 26, 2026
@SnirBroshi
Copy link
Copy Markdown
Collaborator Author

SnirBroshi commented Apr 26, 2026

Hmm, the errors are all due to to_dual having an issue translating a proof:

@[to_dual] failed to insert a cast to make `...` applied to `...` well typed

@github-actions github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 26, 2026
@JovanGerb
Copy link
Copy Markdown
Contributor

JovanGerb commented Apr 26, 2026

Thanks!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 26, 2026

🚀 Pull request has been placed on the maintainer queue by JovanGerb.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 26, 2026
@SnirBroshi SnirBroshi changed the title chore(Order/Hom/Basic): delete redundant EquivLike OrderIso instance chore(Order/Hom/Basic): fix EquivLike OrderIso instance Apr 26, 2026
@JovanGerb JovanGerb changed the title chore(Order/Hom/Basic): fix EquivLike OrderIso instance chore(Order/Hom/Basic): fix EquivLike OrderIso instance diamond Apr 26, 2026
@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Apr 27, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 27, 2026 •
edited
Loading

Benchmark results for cf432da against 10a055a are in. No significant results found. @Vierkantor

  • ✅ build//instructions: -3.6G (-0.00%)

No significant changes detected.

@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Apr 27, 2026

If the benchmark shows no (significant) drawbacks then this looks all good to me and you can borse merge it. (It would be very weird if there is a performance regression. Better spot any issues ahead of time though.)

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Apr 27, 2026

✌️ SnirBroshi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 27, 2026
@SnirBroshi
Copy link
Copy Markdown
Collaborator Author

SnirBroshi commented Apr 27, 2026

Thanks!

bors merge

mathlib-bors Bot pushed a commit that referenced this pull request Apr 27, 2026
@SnirBroshi
chore(Order/Hom/Basic): fix EquivLike OrderIso instance diamond (#3…
f4a1936 
…8559)

`OrderIso` is an `abbrev` for `RelIso` which already has an `EquivLike` instance.
Removing it creates issues with `to_dual`, so instead we make it defeq to the `RelIso` instance using `inferInstance`.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/EquivLike.20OrderIso.20diamond.20w.2F.20to_dual/with/591014670)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented Apr 27, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(Order/Hom/Basic): fix EquivLike OrderIso instance diamond [Merged by Bors] - chore(Order/Hom/Basic): fix EquivLike OrderIso instance diamond Apr 27, 2026
@mathlib-bors mathlib-bors Bot closed this Apr 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@SnirBroshi @JovanGerb @Vierkantor @leanprover-radar @b-mehta