leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

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 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll