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
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 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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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