def k : set ℕ × ℕ := { (1, 2) }

Stream: new members

[Kevin Sullivan]

This simple definition of a set (seems like it) should just work. But it doesn't.

def k : set ℕ × ℕ := { (1, 2) }.

Instead it generates complaints about missing typeclass instances. Thoughts?

[Lean]
failed to synthesize type class instance for
⊢ has_emptyc (set ℕ × ℕ)
[Lean]
failed to synthesize type class instance for
⊢ has_insert ?m_1 (set ℕ × ℕ)
singleton : Π {α γ : Type} [_inst_1 : has_emptyc γ] [_inst_2 : has_insert α γ], α → γ

[Mario Carneiro]

you have precedence wrong

[Mario Carneiro]

def k : set (ℕ × ℕ) := { (1, 2) }

[Kevin Sullivan]

you have precedence wrong

Alas. Thx.