Re: [isabelle] datatype_new_compat produces illegal type



Hi Andreas,

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

> 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. :)

Jasmin





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