Zulip Chat Archive

Stream: general

Topic: decidable equality for strings


view this post on Zulip Thorsten Altenkirch (Feb 18 2021 at 16:01):

How do I activated the decidable equality for strings? I get

22:3: failed to synthesize type class instance for
x : string
 decidable (x == "x")

I tried import init.data.string.instances but it says the path doesn't exist?

view this post on Zulip Kana (Feb 18 2021 at 16:02):

Maybe (x = "x") should be?

view this post on Zulip Thorsten Altenkirch (Feb 18 2021 at 16:05):

Ok, I forgot that Lean is this clever way of overloading Prop and bool. Is this written up somewhere?

view this post on Zulip Eric Wieser (Feb 18 2021 at 16:06):

== is not a bool either, its docs#heq

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 16:06):

And decidable expects a Prop anyway


Last updated: May 14 2021 at 04:22 UTC