[isabelle] Nitpick/Quickcheck Domain



Hello,

if

domain B = b | c

lemma "forall a. a = b"
nitpick
quickcheck

then one would expect a counterexample "a := c".
How can I make nitpick and quickcheck find it?

Thank you!



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