On Mon, 26 May 2014, Jasmin Blanchette wrote:
Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel <tray...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
