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



Am 30.06.2011 um 16:06 schrieb Makarius:

> On Thu, 30 Jun 2011, Alexander Krauss wrote:
> 
>> Or, which is probably easier, you use the "rep_datatype" command to instruct the system to regard the record type you defined as a datatype: After the record definition, do
>> 
>> rep_datatype Foo_ext by (fact Foo.ext_induct) (fact Foo.ext_inject)
> 
> Strictly speaking, this exposes implementation details of version 12 of the record package (or is it version 17).  It should work for now, but nobody can say when there will be the next change in the internal representation.

If we go for the above, version 13 of the record package (or was it 18) will have to make sure it can also register itself as a datatype; otherwise the tests would fail and it would not get pushed to the repository in the first place. It's hard to imagine a reasonable implementation of records that wouldn't provide those very basic properties in some form that can be used by Isabelle's automatic tactics if not "rule".

Jasmin






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.