Re: [isabelle] Problems with datatype_compat



Hi René,

Am 05.08.2014 um 12:20 schrieb René Thiemann <rene.thiemann at uibk.ac.at>:

> I encountered the following problem when using datatype_compat:
> 
> datatype_new 'a tree = Empty | Node 'a "'a tree list"
> datatype_compat tree
> 
> datatype_new 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
> datatype_compat ttree
> 
> exception TYPE raised (line 329 of "~~/src/HOL/Tools/hologic.ML"):
> dest_prodT
> (('a ttree × 'b) list tree × 'd) list
> [...]
> 
> The problem occurs with both Isabelle2014-RC1 and -RC2.
> The datatypes can be also be found in $AFP/thys/Datatype_Order_Generator/Derive_Examples.

Thanks for the report! Dmitriy and I have been looking more closely at the issue but we haven't been able yet to determine if it's his bug or mine. ;) Hopefully we'll be able to come back to you in the coming days with a fix. Regarding the Isabelle2014 release, I fear we won't be able to include a fix, since this isn't a regression and we must be very conservative in our changes so close to a release.

As usual, sorry for the trouble.

Cheers,

Jasmin





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