Currently we have
definition
of_real :: "real ⇒ 'a::real_algebra_1" where
"of_real r = scaleR r 1"
Maybe of_real could be done another way.
And floats could be injected into the rationals.
Larry
> On 29 Jul 2015, at 16:34, Johannes Hölzl wrote:
>
> Ah, I forgot about real of float.
>
>
Ah, I forgot about real of float.
I assume you meant:
of_float :: float => 'a::field
- Johannes
Am Mittwoch, den 29.07.2015, 16:07 +0100 schrieb Larry Paulson:
> This is an unusual case, because this function is not even injective. I would
> prefer to reserve of_XXX for generic functions, l
This is an unusual case, because this function is not even injective. I would
prefer to reserve of_XXX for generic functions, like the existing ones.
I now see that there is another case:
real :: float => real
This one is injective, and a properly generic function
of_float :: "
I'm fine with it. The only problem maight be that
real :: "ereal => real"
is overloaded in Extended_Real, which is quite often used in Probability
theory. I can rename it to "of_ereal".
- Johannes
Am Mittwoch, den 29.07.2015, 15:02 +0100 schrieb Larry Paulson:
> In recent work, I’ve seen agai
In recent work, I’ve seen again how tricky things are with coercions. We need
“real” because it is already used in thousands of places and in many basic
lemmas, but it can only do nat=>real and int=>real. If we are working more
abstractly, only of_nat and of_int are general enough. It isn’t unus
