Email Gateway (Aug 22 2022 at 14:05): Email Gateway (Aug 22 2022 at 14:05):From: Corey.Lewis@data61.csiro.au
Hi all,
As far as I can tell, I seem to have run into an issue with the datatype
package. After slightly increasing the complexity of an existing
datatype I get a 'Proof failed' error message.
The problematic datatype is
datatype ('s, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list"
Cheers,
Corey
Test.thy
Email Gateway (Aug 22 2022 at 14:05):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Corey,
The bug appears to be already fixed in the development version of Isabelle, and hence in the forthcoming release (expected before the end of the year). There should be easy (but ugly) workarounds, e.g. by using a type isomorphic to ×. Let me know if you want a patch for Isabelle2016.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 14:05):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Dear Corey,
another (much simpler) workaround is to put a “dead” annotation on ’s (it is dead anyway since it occurs as a parameter to set):
datatype (dead 's, 'p) test' =
Test' "(('s, 'p) test' × 's set × 's set) list”
Cheers,
Dmitriy
Email Gateway (Aug 22 2022 at 14:05):From: Corey.Lewis@data61.csiro.au
Awesome, thanks Dmitriy! That solves my problem nicely.
Cheers,
Corey
Last updated: Apr 23 2024 at 20:15 UTC