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.haftm...@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
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
