Re: [isabelle] datatype_new_compat requires sort type



Hi Jasmin,

Thanks for fixing. I currently don't see the need to change my Isabelle2012-2 installation, as I don't know of an example of a datatype that falls in the scope of datatype_new_compat and that absolutely needs sort constraints on type variables. (I have some BNFs that need sort constraints, but datatype_compat_new cannot handle recursion through these.)

Andreas

On 09/01/14 14:18, Jasmin Blanchette wrote:
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.