Generate Set from List

Stream: new members

[Christian K]

Is there a way to generate a List from a (possibly infinte) Set so that it includes every element of the Set?

def list_from_set {α : Type} (x : Set α) : List α := by sorry
def lst := list_from_set {1,2,3,4}  -- -> [1,2,3,4]
def lst2 := list_from_set {x : ℕ | x > 2} -- -> [list with all Natural numbers > 2]

[Simon Daniel]

there is a Function Finset.toList for Finsets docs
i dont know if i remember correctly, but i think Lists have to be finite

[Ruben Van de Velde]

Yes, a List is finite

[Christian K]

Ok, makes sense. I figured out another way to get around using a list, thank you for the clarification.