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.


	Makarius





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