Re: [isabelle] Nitpick/Quickcheck Domain



Dear Rene, thank you for the answer.
"Datatype" as Keyword works.
The question is, how do we get quickcheck and nitpick to work with the
Domain-Keyword of HOLCF.

On Thu, Apr 4, 2019 at 8:53 AM Thiemann, René <Rene.Thiemann at uibk.ac.at>
wrote:

> 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!
>
>



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