Hi Jasmin,
On 14/03/14 14:18, Jasmin Blanchette wrote:
Another candidate is "Quickcheck_Narrowing.thy". Nothing in "HOL" seems to
depend on it, and (please correct me if I'm mistaken) hardly anybody go into the trouble of setting
up Quickcheck (and GHC) so that it uses the narrowing strategy.
I guess I am the exception to the rule. I have GHC set up and sometimes try
quickcheck[narrowing]. Sometimes, it does give better results than the random and
exhaustive generators. To make one's type work with narrowing, however, is hardly
documented. Recently, I finally got around to provide narrowing generators for Coinductive
in the AFP (AFP/1fffd2ebbd28), but I had to study all the implementation of the narrowing
engine and read up on SmallCheck in order to understand just how to do it. We definitely
cannot expect most users to figure this out themselves.
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
