Re: [isabelle] Type Coercions?

Christian Doczkal wrote:
>> Yes, it would be nice to have coercions inserted automatically. But no
>> such luck in Isabelle.
> Tanks for the reply. Just out of curiosity. Are there any theoretical or
> deep technical reasons against having this feature or has this simply
> never occurred on a top position on the priorities list? 

No theoretical problem at all. Practically it is not hard either, and we
have thought about it from time to time.

>From a user perspective it can be helpful, but it has it's snags as
well: writing "sin(m+n)", where m,n::int, the system may turn this into
"sin(real(n+m))" or "sin(real m + real n)". Depending on the context,
one may be preferable to the other...


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