Am 26.05.2014 12:53, schrieb Makarius:
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on
options one
could invent long / explicit keywords for them (or Parse.literal
items).
grep gives 371 occurences of "-:" in IsaFoR's development repository.
So it's not a rare add-on, but an important performance optimization.
If it is only an optimization it is conceptually still "rare". But of
course it is also possible to invent short keywords -- after some
empricial studies about the danger of clashing with common identifiers.
The datatypes manual calls the above "dead" so that is an obvious
choice to try out.
Yes, we have considered this naming earlier. It was discarded, because
it looks like one is giving the name "dead" to a set function. The same
holds for any other identifier (not only the common ones). That was the
reason to use something that is not an identifier.
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
