Disjoint union of finsets

Stream: Is there code for X?

[Yaël Dillies]

I have two finsets s and t that I know to be disjoint. How can I make their union without bothering the end user with decidability assumptions?

[Yaël Dillies]

In my case, it's actually making a finset (α ⊕ β) from s : finset α and t : finset β.

[Anne Baanen]

Probably best to directly use the constructor, i.e. finset.mk (s + t : multiset α) sorry, where sorry is something like docs#multiset.nodup_add_of_nodup

[Yaël Dillies]

I'll define finset.sum then.

[Yaël Dillies]

Urgh, finset.sum is obviously already a thing.

[Anne Baanen]

Semi-serious option: finset.add to generalize + on multisets?

[Yaël Dillies]

But what about the α ⊕ β-specific operation? I'm thinking of finset.disj_sum

[Yaël Dillies]

Actually, my original idea doesn't work because disjoint on finsets requires decidable_eq because it goes through the semilattice_inf instance.

[Yaël Dillies]

Back when we had finset.disjoint, this wouldn't have been a problem.

[Yaël Dillies]

Actually, docs#finset.disj_union is already a thing