[isabelle-dev] »real« considered harmful

[Larry Paulson]

Yes, except you won’t be able to find an injection

	»of_float :: float => 'a::field« 

since there are finite fields. Maybe field_char_0 will be sufficient.

Who wants to actually do this?

Larry

> On 6 Aug 2015, at 11:05, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> A conclusion of what I have understood so far:
> * A new »of_float :: float => 'a::field« is provided (btw. »float« could
> be also constructed from the rationals rather than the reals).
> * »real« is restricted to »real :: nat => real« (which corresponds
> nicely to »int :: nat => int«).
> * The special case real [ereal] is renamed, e.g. »the_real :: ereal =>
> real« (cf. enat)
> * Other occurences of real are substituted (if coercions do not save the
> work).
> 
> 	Florian
> 
> -- 
> 
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>