[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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and