Construct finset from set

Stream: Is there code for X?

[Marcus Rossel]

Is there a way of directly constructing a finset from a set and a proof that this set is finite?
Something like:

def f : finset nat := {
  s := some_set
  proof := begin ... end -- some_set.finite
}

[Rémy Degenne]

See docs#set.finite.to_finset

[Marcus Rossel]

That's what I'm using at the moment, but that isn't quite what I want, because then I have to split the definition into a lemma and a definition:

lemma proof : some_set.finite := begin ... end

def f : finset nat := proof.to_finset

[Eric Wieser]

You can combine those in a single definition with have

[Marcus Rossel]

@Eric Wieser
How?

[Eric Wieser]

def f : finset nat :=
have proof : some_set.finite := begin ... end,
proof.to_finset