[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode
Thomas.Sewell at nicta.com.au
Fri Jul 1 06:38:34 CEST 2011
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.
More information about the isabelle-dev