decidable equality for strings

Stream: general

[Thorsten Altenkirch]

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?

[Kana]

Maybe (x = "x") should be?

[Thorsten Altenkirch]

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

[Eric Wieser]

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

[Yakov Pechersky]

And decidable expects a Prop anyway