Zulip Chat Archive

Stream: new members

Topic: has_coe ℝ ℝ


Frédéric Dupuis (Aug 23 2020 at 14:28):

I just started working on the is_R_or_C typeclass, and in the class definition I'd like to require [has_coe ℝ K]. However, when I try to instantiate this with the reals, I get the error that has_coe ℝ ℝ is not registered as an instance. Is this intended behavior? For what it's worth, registering it locally doesn't seem to cause any problems.

Mario Carneiro (Aug 23 2020 at 20:10):

It is problematic, because it will make has_coe_t R ? loop

Frédéric Dupuis (Aug 23 2020 at 20:24):

I see. Oddly enough changing the requirement to has_coe_t ℝ K doesn't work either, it still complains that has_coe_t ℝ ℝ is not an instance. Is there a good way to do this?

Mario Carneiro (Aug 23 2020 at 20:29):

My suggestion would be not to add any coercion and instead use a local notation

Frédéric Dupuis (Aug 23 2020 at 21:16):

What sort of thing do you have in mind? I would like to make statements that apply to the coercion from ℝ to ℂ, and that would also hold for ℝ itself.

Mario Carneiro (Aug 23 2020 at 21:29):

The easy thing to do is to just have and use a function of_real : R -> K

Mario Carneiro (Aug 23 2020 at 21:30):

but this has a lot of notational overhead. If you decide this matters you can do local notation `funny up arrow` := of_real

Frédéric Dupuis (Aug 23 2020 at 21:31):

And then, when I register the instance is_R_or_C ℂ, I would plug in the coercion into of_real?


Last updated: Dec 20 2023 at 11:08 UTC