Email Gateway (Aug 18 2022 at 12:08): Email Gateway (Aug 18 2022 at 12:08):From: John Matthews <matthews@galois.com>
I'd like to use quickcheck and autoquickcheck when proving theorems
inside locales. I'm using Isabelle2008. For example:
locale l =
fixes a::nat
begin
fun foo :: "nat => nat" where
"foo 0 = 0"
| "foo (Suc n) = a + foo n"
end
lemma (in l) "foo n = a * n"
quickcheck
However, quickcheck complains with the following error:
*** Unable to generate code for term:
*** arbitrary
*** required by:
*** locale_quickcheck.l.foo_sumC, locale_quickcheck.l.foo, <Top>
*** At command "quickcheck".
Apparently the [code] attribute for foo that is installed by the
function package is not being applied to l.foo.simps?
Thanks,
-john
Last updated: Nov 21 2024 at 12:39 UTC