Zulip Chat Archive

Stream: maths

Topic: decidable problem


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Feb 19 2021 at 10:13):

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

view this post on Zulip Eric Wieser (Feb 19 2021 at 10:15):

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

view this post on Zulip 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