[isabelle] quickcheck in locales
I'd like to use quickcheck and autoquickcheck when proving theorems
inside locales. I'm using Isabelle2008. For example:
locale l =
fun foo :: "nat => nat" where
"foo 0 = 0"
| "foo (Suc n) = a + foo n"
lemma (in l) "foo n = a * n"
However, quickcheck complains with the following error:
*** Unable to generate code for term:
*** 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and