Quoting Alex:
Someone who knows more about records can probably explain why this
declaration isn't issued internally by default...
I suppose everyone is expecting that someone to be me. It's not. The
record package is huge, and I didn't have a clear idea of all the
applications it had, so I left as much of the interface as possible
unchanged. I guess I did remove some inner constants, but they were
clearly meant to be implementation details.
The 'ext' constant, which constructs the (| a = 1, b = 2 |) style
syntax, looks like it's been there a while. Assuming this syntax is used
in the future, it will probably be backed by a constant. Naming it as a
constructor would seem reasonable, but I have no idea what the
ramifications would be. I don't know anything at all about the internals
of the datatype package.
The only concern I can see is a potential performance problem with the
datatype package - there are some very large records in use. At least
one, anyway. I did consider at one point adding a flag which would turn
off some features of the package for users concerned about performance.
This would make it easier to add new features in if needed.
Yours,
Thomas.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
