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