[isabelle-dev] Notes on datatype_new list

[Makarius]

On Mon, 26 May 2014, Jasmin Blanchette wrote:

> Am 26.05.2014 um 15:24 schrieb Makarius <makarius at sketis.net>:
>
>> 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.
>
> Indeed, that would make sense. And perhaps we don't even need to make it 
> a keyword? It shouldn't be hard to parse "(dead 'a)" with 
> "Parse.reserved" for "dead".

In principle yes.  The final answer is left to the one who goes to the 
bottom of the system to implement it -- and sees if there are other 
side-conditions.

Note that in PIDE there is extra markup even for certain quasi-keywords, 
e.g. the "add" in "(simp add: ...)".


 	Makarius