On Fri, 1 Mar 2013, Lawrence Paulson wrote:
In Edinburgh LCF, term quotations containing anonymous type variables
were simply rejected. Perhaps that would still be the best approach now.
I'm not convinced that it would lead to more errors than the 'a itself
approach.
I know, you've explained that to me many years ago.
For us now, it means to mark-up these critical spots where polymoprhism
emerges. The information can then be somehow visualized for the user.
It is also possible to get a systematic overview over all reachable
Isabelle applications (including AFP) how things actually happens in the
wild.
The latter is not just for empirical exploration of sources. With formal
markup of certain kind over the text, that can be "refactored"
systematically. I am here not so much thinking of eliminating legitimate
uses of polymorphism, but things like cleaning up notation to avoid the
mix of --> and ⟶ symbols.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
