Email Gateway (Aug 22 2022 at 15:19): Email Gateway (Aug 22 2022 at 15:19):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I stumbled over a funny thing today: Even if a value x is not of record
type, record update syntax will still work. For example,
x (| v := t |)
works as long as a constant v_update with the appropriate type is in scope.
Should the datatype command be extended to produce these constants? It
is quite convenient syntax (which can't be said of records in general).
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:19):From: Lars Hupel <hupel@in.tum.de>
Hi,
By default, I'd say clearly no. The (co)datatype package already
generates more than enough constants and theorems as it is.
sure, that's true. If it were implemented I guess that'd go into a
plugin anyway. (I have many things that should go into a plugin at some
point ...)
I suggest we just keep this as an idiom. If more than one person ends
up using this, and the general parsing principle you describe is
considered a feature of the system and not a bug, we could add a
brief section to the manual.
Right. I know very little about the record package apart from that it is
not localized and does not register itself as a BNF (for which there is
"copy_bnf" these days, luckily). I also don't know if someone still
feels responsible for it.
I should probably motivate why this came up: Lem (the specification
language) is able to generate records in Isabelle. I had to change some
of them to datatypes and then realized that the syntax would still work.
(Lem does not use extensible records so they should probably generate
datatypes directly.)
But I'm happy to leave things as they are right now. Maybe somebody on
this list has already done something like that.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:19):From: Thomas.Sewell@data61.csiro.au
Not directly relevant to this discussion, but:
This additional faux record syntax is used in a number of developments.
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 15:19):From: Makarius <makarius@sketis.net>
This was done on purpose many years ago, when this notation was
introduced. A bit later, the record package turned out the canonical
source of such update functions, but there are (very few) other
applications found elsewhere.
Makarius
Last updated: Apr 23 2024 at 20:15 UTC