andreas.lochbihler at inf.ethz.ch
Fri Mar 14 15:26:30 CET 2014
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.
More information about the isabelle-dev