[isabelle] Quickcheck for HOLCF domains?
I would like to use Isabelle's quickcheck facility for quickly testing
lemmas in HOLCF before attempting to prove them. This seems to work
fine for the simple lemma
lemma "(LAM x. x) $ (Def x) = Def x"
However, Isabelle's code generator doesn't seem to know what to do with
constructors generated by HOLCF's domain package. Here is an example
that the quickcheck method can't handle:
domain D = B | C
lemma "(LAM x. x) $ B = B"
(I'm using development snapshot Isabelle_13-Jul-2005.) Instead,
Isabelle generates the following error message:
*** Unable to generate code for type:
*** required by:
*** At command "quickcheck".
What is needed to add support for HOLCF's domain package to Isabelle's
This archive was generated by a fusion of
Pipermail (Mailman edition) and