Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with quickcheck: exception Match raise...

Email Gateway (Aug 22 2022 at 15:46):

From: Sebastiaan Joosten <sjcjoosten@gmail.com>
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

Last updated: Apr 25 2024 at 04:18 UTC