Re: [isabelle] Nitpick/Quickcheck Domain



Dear Rei,

I’m not sure where the actual problem is:

theory Test
imports Main
begin

datatype B = b | c

lemma "∀ a. a = b”
nitpick (* reports counterexample *)
quickcheck (* reports counterexample *)

end

Best,
René



> Am 30.03.2019 um 00:41 schrieb Rei Kristo <reikristo at gmail.com>:
> 
> 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!

Attachment: signature.asc
Description: Message signed with OpenPGP



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