[isabelle-dev] Additional type variable(s) in specification
makarius at sketis.net
Thu Dec 2 17:46:20 CET 2010
On Thu, 2 Dec 2010, Brian Huffman wrote:
> But if we had something like a "fixes" clause for types, it would look
> nicer and indicate the intention unambiguously, making a warning message
> locale count = fixes_type 'a assumes ex_inj: "EX f::'a => nat. inj f"
This would be a substantial change in the way "polymorhphism" works in the
system. IIRC, Moscow ML introduced such an extension to Hindley-Milner
typing and consequently caused some serious breakdown.
More information about the isabelle-dev