[isabelle-dev] Notes on datatype_new list

[Makarius]

On Mon, 26 May 2014, Jasmin Blanchette wrote:

> Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel <traytel at in.tum.de>:
>
>> 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.
>
> Right. On the other hand, it's hard to imagine anybody giving the name 
> "dead" to the set of values associated with a so called *live* type 
> variable, so perhaps it's not too bad a choice.

This is presently Parse.reserved (i.e. a plain identifier) followed by a 
colon.  Thus it conforms to similar method section syntax like
(simp add: ...)

I think you could afford an actual keyword for the "dead" modifier and use 
it without colon, like "lazy" in HOLCF/domain.  That would substract 
"dead" from the normal identifier space, but merely means its very few 
occurrences on AFP/Jinja and AFP/JinjaThreads need to be quoted.


 	Makarius