Hallo Fabian,
This is the issue that was discussed here:
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2022-03/msg5.html
In short, I broke this in 2014 when moving to the new datatypes and it's not
easy to repair. I doubt I will ever find the time to do it myself -- it
requires some
In the following minimal example:
datatype t = A | B "t × t"
fun f :: "t ⇒ bool" where
"f A ⟷ True"
| "f _ ⟷ False"
quickcheck throws an error if you invoke it (both Isabelle2022 and
latest devel):
lemma "f x = True" quickcheck
Does anyone have an idea what's going on? The error is as
