Re: [isabelle] "Coercion inference failed"
On Thu, 31 Mar 2011, Eg Gloor wrote:
I see. So Isabelle/HOL isn't truly polymorphic since there isn't type
quantification. Could you provide some pointers to material explaining
the naive polymorphism?
You can probably find a lot of references just by searching through the
archives of the isabelle-users mailing list -- this is a recurrent topic.
Just one arbitray paper where the topic is also mentioned
http://www4.in.tum.de/~wenzelm/papers/local-theory.pdf -- it is about
giving an impression of Hindley-Milner polymorphism in a system with plain
schematic types only.
This archive was generated by a fusion of
Pipermail (Mailman edition) and