Re: [isabelle] Sublocale, subclass and execution.



Thank you for the useful response.

2014-10-09 16:02 GMT+02:00 Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de>:

>
> Note that the unexpected »real« type is due to an implicit coercion.
>
>
Is there any feasible way to avoid that implicit coercion?
As far as I know, using permanent_interpretation gcd_eucl is now executable
but only over fields. Am I right?

I mean:

value "gcd_eucl (13::nat) (6::nat)"

Computes "field_class.gcd_eucl (real 13) (real 6)", which is unsatisfactory
for my purposes, because the gcd_eucl over reals is not the same as the
gcd_eucl over int or nat. I guess that now "euclidean_semiring.gcd_eucl"
has been hidden by the permanent_interpretation.

Thanks,
Jose



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.