[isabelle-dev] »real« considered harmful
lp15 at cam.ac.uk
Thu Aug 6 11:19:11 CEST 2015
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?
> 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
> PGP available:
More information about the isabelle-dev