[isabelle-dev] Notes on datatype_new list
makarius at sketis.net
Mon May 26 15:24:44 CEST 2014
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.
More information about the isabelle-dev