From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF implementors,
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"
Best,
Andreas
From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
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
From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Mar 28 2024 at 16:17 UTC