decidable problem

Stream: maths

[Xavier Xarles]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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