Re: [isabelle] Sublocale, subclass and execution.

Hi Jose,

> Is there any feasible way to avoid that implicit coercion?

you can deactivate it using

declare [[coercion_enabled = false]]

to eliminate a potential source of confusion.

> Computes "field_class.gcd_eucl (real 13) (real 6)", which is
> 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 is only a matter of name space.  You may use

declare [[names_long]]

to have names always printed qualified, this might help in identifying
things which might have been shadowed.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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