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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and