Skip to content

[Merged by Bors] - chore(Finset/Basic): drop an unneeded DecidableEq assumption #25431

[Merged by Bors] - chore(Finset/Basic): drop an unneeded DecidableEq assumption

[Merged by Bors] - chore(Finset/Basic): drop an unneeded DecidableEq assumption #25431

Annotations

1 warning

Lint style

succeeded Mar 30, 2024 in 44s