HasCompl for Finsets?

Stream: mathlib4

[Michael Stoll]

It appears that there is no HasCompl instance for Finsets in Mathlib:

import Mathlib

variable {α : Type*} [Fintype α]
-- failed to synthesize  HasCompl (Finset α)
#synth HasCompl (Finset α)

Is this by design or just an omission? @Yaël Dillies

[Yaël Dillies]

You are missing [DecidableEq α]

[Michael Stoll]

OK, silly me...

[Kevin Buzzard]

We need a bot to post "did you forget DecidableEq?" every time someone asks a question about finsets which doesn't mention it anywhere :-) (I am also guilty of this).

[Yaël Dillies]

Am I not already that bot? :innocent:

[Kevin Buzzard]

Actually we need a bot to write bundled nonconstructive finiteness :-) (plus the 5000 lines of API)

[Ruben Van de Velde]

5000 sounds like a very low guess

[Eric Wieser]

More realistically, changing lean to say "I tried $instance_in_mathlib but it needed DecidableEq which I couldn't find"

[Kevin Buzzard]

We'd have to avoid getting thousands of "I tried TopologicalRing.toRing but nobody ever mentioned topology", which is tried and fails probably many thousands of times in mathlib.

[Eric Wieser]

This has been discussed before; we could tag instances on whether they make sense to warn about in the message. For Finset.instCompleteLattice, this is always something sensible to warn about

[Eric Wieser]

(this doesn't require a change to the search algorithm, just to the error message generation)