finset union

Stream: new members

[Patrick Thomas]

How would I take the finset union over a function from fin n to finset? That is, I think I want ∪_{i : fin n}, f i where f: fin n -> finset.

[Kevin Buzzard]

Is it docs#finset.bUnion ? Yeah that'll do it, use finset.univ to get all of fin n as a finset

[Eric Wieser]

If you don't care about computability ⨆ i, f i will work

[Patrick Thomas]

So like:

inductive term : Type
| var : string → term
| func {n} : string → (fin n → term) → term

def term.all_var_set : term → finset string
| (var x) := {x}
| (func f args) := finset.bUnion finset.univ (fun i, term.all_var_set (args i))

?

[Patrick Thomas]

I think I care about computability here.

[Patrick Thomas]

Thank you.

[Eric Wieser]

That looks good to me

[Patrick Thomas]

Great! Thank you!