## Stream: maths

### Topic: decidable problem

#### Xavier Xarles (Feb 19 2021 at 10:09):

I want to define a (S → R)  where R has a zero , (r : R) and (a:S) , by sending a to r and the rest to 0. I tried

example {S : Type*} {R : Type*} [has_zero R] (a : S) (r : R) : (S → R):=
λ b, if a = b then r else 0


but lean says that

failed to sinthetize type class instance for
decidable (a = b)


Any suggestion what to do?

#### Johan Commelin (Feb 19 2021 at 10:13):

@Xavier Xarles open_locale classical at the top of your file (-;

#### Eric Wieser (Feb 19 2021 at 10:15):

Or, add [decidable_pred ((=) a)] or [decidable_eq S]

#### Eric Wieser (Feb 19 2021 at 10:16):

Note that that function is precisely docs#pi.single, as pi.single a r

Last updated: May 11 2021 at 16:22 UTC