Re: [isabelle] datatype_new_compat produces illegal type

Hi Andreas,

Am 14.11.2013 um 16:27 schrieb Andreas Lochbihler <andreas.lochbihler at>:

> 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?

Fixed (4a655e62ad34). Thanks for the report!

And I'm of course glad to see you're using the new-style datatypes. :)


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