Zulip Chat Archive

Stream: new members

Topic: has_coe ℝ ℝ


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

view this post on Zulip Mario Carneiro (Aug 23 2020 at 20:10):

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

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

view this post on Zulip Mario Carneiro (Aug 23 2020 at 20:29):

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

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

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

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

view this post on Zulip 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: May 16 2021 at 21:11 UTC