finset.sUnion

Stream: maths

[Scott Morrison]

I can't find any sign of finset.sUnion : finset (finset A) -> finset A. Am I missing something?

[Kenny Lau]

bind

[Chris Hughes]

It might be join

[Scott Morrison]

Hmm... bind isn't quite what I want, it's

def bind (s : finset α) (t : α → finset β) : finset β

[Scott Morrison]

and I can't find any sign of finset.join.

[Scott Morrison]

but I guess s.bind id will do.

[Scott Morrison]

Shall I just add join defined as that?

[Scott Morrison]

or am I meant to set up a monad instance?

[Kenny Lau]

#find doesn't give me anything

[Mario Carneiro]

I wouldn't mind calling this sUnion instead of join. We mostly use set theoretic terminology in finset

[Mario Carneiro]

I'm pretty sure I've used bind id for this in the past, without bothering with a definition