has_coe ℝ ℝ

Stream: new members

[Frédéric Dupuis]

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]

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

[Frédéric Dupuis]

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]

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

[Frédéric Dupuis]

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]

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

[Mario Carneiro]

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]

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