[isabelle] Exception in code generator
I'm now trying to define an overloaded Cryptol constant that is
supposed to return zero on all types, but quickcheck's code generator
seems to be failing on one of the overloaded definitions. Here is a
class czero_ty = type +
fixes czero :: "'a"
instance bool :: czero_ty
czero_bool_def: "czero == False"
instance "fun" :: (type,czero_ty)czero_ty
czero_fun_def: "czero n == czero"
When I try to test "(czero :: int => bool) n = False" with quickcheck,
I get the following error:
*** Unable to generate code for term:
*** required by:
*** czero_quickcheck.czero_ty_class.czero def1, <Top>
*** At command "quickcheck".
I think the problem is in czero_fun_def, because if I try to execute
then Isabelle returns this exception:
*** exception TERM raised: dest_Trueprop
*** At command "declare".
I'm using Isabelle2007.
This archive was generated by a fusion of
Pipermail (Mailman edition) and