Re: [isabelle] Type Coercions?

On Fri, 2009-03-27 at 09:43 +0100, Tobias Nipkow wrote:
> Christian Doczkal wrote:
> >> Yes, it would be nice to have coercions inserted automatically. But no
> >> such luck in Isabelle.

"Trueprop" comes close, doesn't it?  To me it looks like an invisible
coercion from bool to prop.  But I'll admit that I have no idea how it
works internally, or why this can't be made to work for other coercions.

> >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...

One might want to look at algorithms for overload resolution (in Ada/

(Isn't "real (m+n)" equal to "real m + real n" anyway, so that it makes
no difference in the above example?)


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