no `has_insert` for `finset`

Stream: general

[Chris Hughes]

example {α : Type*} : has_insert α (finset α) := by apply_instance -- doesn't work

Shouldn't there be a has_insert instance on finset? Without it I can't use the notation {0,1,2}

[Mario Carneiro]

there is an insert operation, but it requires decidable_eq