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

fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument #2918

Merged
merged 1 commit into from
Nov 20, 2023
Merged

fix: DecidableEq deriving handler could not handle fields whose types start with an implicit argument #2918

merged 1 commit into from
Nov 20, 2023

Conversation

kmill
Copy link
Collaborator

@kmill kmill commented Nov 20, 2023

Fixes #2914

@kmill kmill requested review from leodemoura and Kha as code owners November 20, 2023 04:07
@kmill kmill force-pushed the fix_2914 branch 2 times, most recently from b6b7110 to cc67737 Compare November 20, 2023 04:26
@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 20, 2023
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 20, 2023
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2918
1747783
@kmill kmill added the awaiting-review Waiting for someone to review the PR label Nov 20, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 20, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

@kim-em kim-em merged commit 4d39a0b into leanprover:master Nov 20, 2023
LeoDog896 added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 28, 2024
@LeoDog896
chore(Combinatorics/Enumerative/Partition): auto-drive DecidableEq
db35bb0 
Original bug fixed in leanprover/lean4#2918.
@LeoDog896 LeoDog896 mentioned this pull request Dec 28, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 5, 2025
@LeoDog896
chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#…
8a6db46 
…20277)

Original bug fixed in leanprover/lean4#2918.




Co-authored-by: Tristan F. <LeoDog896@hotmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@timotree3 timotree3 timotree3 left review comments

@kim-em kim-em kim-em approved these changes

@leodemoura leodemoura Awaiting requested review from leodemoura

@Kha Kha Awaiting requested review from Kha

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR 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.

Deriving DecidableEq fails in implicit argument
4 participants
@kmill @leanprover-community-mathlib4-bot @kim-em @timotree3