Re: [isabelle] Nitpick/Quickcheck Domain



I see.

Perhaps You or Mr.Blanchette could help me by recommending / forwarding the
question to someone?

It would also be interesting to learn more about the following related but
unanswered old question of John Matthews:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2005-September/msg00016.html

Thank You!

On Sat, Apr 6, 2019 at 6:54 AM Thiemann, René <Rene.Thiemann at uibk.ac.at>
wrote:

> Hi Rei,
>
> > "Datatype" as Keyword works.
> > The question is, how do we get quickcheck and nitpick to work with the
> Domain-Keyword of HOLCF.
>
> Ah, now I understand that you are referring to HOLCF.
>
> Sorry, I don’t know the internals of HOLCF’s “domain” and how to connect
> it with quickcheck/nitpick.
>
> René
>



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