[isabelle-dev] [isabelle] Error: Non-constructor pattern not allowed in sequential mode

Thomas Sewell Thomas.Sewell at nicta.com.au
Fri Jul 1 06:38:34 CEST 2011

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.


More information about the isabelle-dev mailing list