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
unnecessary:
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
