Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] datatype_new_compat produces illegal type

Email Gateway (Aug 19 2022 at 12:30):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF experts,

In Isabelle2013-1, I tried datatype_new_compat on the following example:

theory Scratch imports "~~/src/HOL/BNF/BNF" begin
datatype_new ('out, 'in) event = Event 'out 'in
datatype_new_compat event

Unfortunately, I get the following error upon datatype_new_compat:

*** Illegal type for constant "Scratch.event.event_rec" :: ('c => 'd => nat) => ('a, 'b)
event => nat
*** The error(s) above occurred in axiom "event_size_def"
*** At command "datatype_new_compat"

What am I doing wrong here?

Best,
Andreas

Email Gateway (Aug 19 2022 at 12:30):

From: Dmitriy Traytel <traytel@in.tum.de>
Nothing. It's a failure on our side that we'll investigate. Thanks for
noticing.

As a temporary workaround the following works:

datatype_new ('a, 'b) event = Event 'a 'b
datatype_new_compat event

Dmitriy

Email Gateway (Aug 19 2022 at 12:30):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Dmitriy,

Thanks for the quick reply and the simple workaround.

Best,
Andreas

Email Gateway (Aug 19 2022 at 12:30):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,

Fixed (4a655e62ad34). Thanks for the report!

And I'm of course glad to see you're using the new-style datatypes. :)

Jasmin

Last updated: Apr 19 2024 at 01:05 UTC