Skip to content

[Merged by Bors] - chore(Data/List): fix decidable instance for List.Chain#24515

Closed
erdOne wants to merge 2 commits intomasterfrom
erd1/listDecidable
Closed

[Merged by Bors] - chore(Data/List): fix decidable instance for List.Chain#24515
erdOne wants to merge 2 commits intomasterfrom
erd1/listDecidable

Conversation

@erdOne
Copy link
Copy Markdown
Member

@erdOne erdOne commented May 1, 2025

Previously it did rewrites on the data so it didn't work.


Open in Gitpod

@erdOne erdOne requested a review from b-mehta May 1, 2025 14:43
@github-actions
Copy link
Copy Markdown

github-actions bot commented May 1, 2025

PR summary 6b05e65b4c

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/declarations_diff.sh <optional_commit>

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

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


No changes to technical debt.

You can run this locally as

./scripts/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-data Data (lists, quotients, numbers, etc) label May 1, 2025
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@b-mehta b-mehta added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label May 1, 2025
@erdOne erdOne added auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. and removed auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. labels May 1, 2025
@ghost
Copy link
Copy Markdown

ghost commented May 1, 2025

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label May 1, 2025
mathlib-bors bot pushed a commit that referenced this pull request May 1, 2025
Previously it did rewrites on the data so it didn't work.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 1, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Data/List): fix decidable instance for List.Chain [Merged by Bors] - chore(Data/List): fix decidable instance for List.Chain May 1, 2025
@mathlib-bors mathlib-bors bot closed this May 1, 2025
@mathlib-bors mathlib-bors bot deleted the erd1/listDecidable branch May 1, 2025 16:39
riccardobrasca pushed a commit that referenced this pull request May 7, 2025
Previously it did rewrites on the data so it didn't work.
tannerduve pushed a commit that referenced this pull request May 13, 2025
Previously it did rewrites on the data so it didn't work.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants