Failedd to synthesize type class instance for set.decidab...

Stream: general

[AHan]

In the following example, I don't understand why lean failed to synthesize type class instance for decidable (x ∈ s) ?
What did I miss?

import data.set
universes u
variables {α : Type u}

def f (x : α) (s : set α) : set α := if x ∈ s then {x} else ∅

[Bryan Gin-ge Chen]

if P then _ else _ requires P to be decidable, otherwise how will lean know which branch to take? Here's the discussion in TPiL. One thing you could do is use

open classical
local attribute [instance, priority 0] prop_decidable

[Mario Carneiro]

Another way is to write the set without an if statement, i.e.

def f (x : α) (s : set α) : set α := {y | x ∈ s ∧ y = x}

[AHan]

Thanks a lot!
Both solutions are nice!!

[Kenny Lau]

but the latter is nicer