Re: [isabelle] datatype_new_compat produces illegal type



Hi Dmitriy,

Thanks for the quick reply and the simple workaround.

Best,
Andreas

On 14/11/13 16:43, Dmitriy Traytel wrote:
Am 14.11.2013 16:27, schrieb Andreas Lochbihler:
Dear BNF experts,

In Isabelle2013-1, I tried datatype_new_compat on the following example:

theory Scratch imports "~~/src/HOL/BNF/BNF" begin
datatype_new ('out, 'in) event = Event 'out 'in
datatype_new_compat event

Unfortunately, I get the following error upon datatype_new_compat:

*** Illegal type for constant "Scratch.event.event_rec" :: ('c => 'd => nat) => ('a, 'b)
event => nat
*** The error(s) above occurred in axiom "event_size_def"
*** At command "datatype_new_compat"

What am I doing wrong here?
Nothing. It's a failure on our side that we'll investigate. Thanks for noticing.

As a temporary workaround the following works:

datatype_new ('a, 'b) event = Event 'a 'b
datatype_new_compat event

Dmitriy






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