Commit 2024-04-16 21:36 1aff9ff0
View on Github →chore(Data/Finset/Powerset): Fix decidability instances (#11672)
Typeclass search cannot synthesize ∀ t ⊆ s, Decidable (p t) hypothesis, hence the instance could never fire. Fix it and compress back the binders, both in the instancs and Combinatorics.Additive.SalemSpencer where they were supposed to be used.