## Stream: general

### Topic: no has_insert for finset

#### Chris Hughes (Jul 04 2018 at 16:42):

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 (Jul 04 2018 at 16:49):

there is an insert operation, but it requires decidable_eq

Last updated: May 12 2021 at 23:13 UTC