fintype.insert and decidable_eq

Stream: general

[Eric Rodriguez]

This is in the general docs for finset:

finset.insert and finset.cons: For any a : α, insert s a returns s ∪ {a}. cons s a h returns the same except that it requires a hypothesis stating that a is not already in s. This does not require decidable equality on the type α.

However, insert on finsets does reqiure decidable_eq, which means one of two things happened:

• The requirement for decidable_eq got added later, and could be removed
• The docstring is written wrong

Before I make a PR changing the docstring, can anyone confirm that decidable_eq is indeed needed?

[Yakov Pechersky]

The "This does not require decidable equality" is true with regards to docs#finset.cons, iiuc.

[Floris van Doorn]

docs#finset.has_insert depends on decidable_eq.