[isabelle-dev] smt2

[Andreas Lochbihler]

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