Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] datatype_new_compat requires sort type


view this post on Zulip Email Gateway (Aug 19 2022 at 13:28):

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

view this post on Zulip Email Gateway (Aug 19 2022 at 13:28):

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

view this post on Zulip Email Gateway (Aug 19 2022 at 13:28):

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