Re: [isabelle] datatype_new_compat produces illegal type
Thanks for the quick reply and the simple workaround.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and