Re: [isabelle] datatype_new_compat requires sort type



Hi Andreas,

> I just want to report that in Isabelle2013-2, the datatype_new_compat command fails on datatypes that have been declared with sorts other than {type} on their type variables. Here's a small example.
> 
> theory Scratch imports "~~/src/HOL/BNF/BNF" begin
> 
> default_sort equal
> datatype_new 'a foo = Foo 'a
> datatype_new_compat foo
> 
> *** Type error in application: incompatible operand type
> ***
> *** Operator:  fa :: 'a => nat
> *** Operand:   x :: 'b
> *** The error(s) above occurred in axiom "foo_size_def"
> *** At command "datatype_new_compat"

Thank you for the report. I've just fixed it in the repository version (f00012c20344). It should be easy to apply the change to 2013-2, should that be necessary.

Cheers,

Jasmin





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