equal
deleted
inserted
replaced
409 |
409 |
410 subsection {* Examples with underspecified/partial functions *} |
410 subsection {* Examples with underspecified/partial functions *} |
411 |
411 |
412 lemma |
412 lemma |
413 "xs = [] ==> hd xs \<noteq> x" |
413 "xs = [] ==> hd xs \<noteq> x" |
414 quickcheck[exhaustive, potential = false, expect = no_counterexample] |
414 quickcheck[exhaustive, expect = no_counterexample] |
415 quickcheck[exhaustive, potential = true, expect = counterexample] |
415 quickcheck[random, report = false, expect = no_counterexample] |
416 quickcheck[random, potential = false, report = false, expect = no_counterexample] |
416 quickcheck[random, report = true, expect = counterexample] |
417 quickcheck[random, potential = true, report = false, expect = counterexample] |
|
418 oops |
417 oops |
419 |
418 |
420 lemma |
419 lemma |
421 "xs = [] ==> hd xs = x" |
420 "xs = [] ==> hd xs = x" |
422 quickcheck[exhaustive, potential = false, expect = no_counterexample] |
421 quickcheck[exhaustive, potential = false, expect = no_counterexample] |