[isabelle-dev] Notes on datatype_new list
makarius at sketis.net
Mon May 26 12:53:49 CEST 2014
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.
The BNF package has a slight tendency to cryptic shortcuts to conceal it
from outsiders (like category theory in general).
More information about the isabelle-dev