[isabelle] Problem with quickcheck: exception Match raised (line 98 of "generated code")



I just wanted to report a small problem with quickcheck:

fun f' where "f' (Suc x) = Suc (Suc (f' x))"
lemma "f' 0 = 0 â f' 0 = 1" quickcheck

The output is:
Testing conjecture with Quickcheck-exhaustive... 
exception Match raised (line 34 of "generated code")

(The exception is raised regardless of whether the statement is true or not.)

Regards,

Sebastiaan



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.