Finset questions

Stream: lean4

[Alex Sweeney]

In the Mathlib source code doc comments, Finset says it has both insert and Finset.cons which is the same but also requires a ∉ S. I want something like insert where I can add an element and I don't care if it was already there or not. Finset.cons exists but not Finset.insert nor Finset.union. But I did find a workaround and used Union.union fs {value}. Then I thought maybe Insert.insert fs value would work but it doesn't.

So Union.union can do what I want but it's a little ugly. I guess I have a few questions.

• Why is Finset.cons the only insertion operation included as a def on Finset?
• How is insert supposed to work? The code docs make it seem like it's trivial but I don't get it.

[Kyle Miller]

To use insert value fs (note the argument order, it's opposite of what you have in your message) you need to make sure you have a DecidableEq instance