Hi Jasmin,
On 14/03/14 16:05, Jasmin Blanchette wrote:
Hi Andreas,
Am 14.03.2014 um 15:26 schrieb Andreas Lochbihler
<andreas.lochbih...@inf.ethz.ch>:
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.
How big an issue is it to you if we move narrowing to Library?
I don't mind if narrowing is moved to HOL-Library, I'll just add another theory to my list
of theories that I usually import. If you do so, please make sure that the connection to
the datatype packages is kept, i.e., narrowing generators are generated for all datatypes
(even those that are defined while narrowing was not in scope).
> From what I understand, you already pull in quite a bit from Library, to the extent
that "Coinductive" is based on the "HOL-Library" session. And Quickcheck has a nice
generic interface for registering "testers" at any point, so technically the move should
be nearly trivial.
IIRC, the AFP policy is (was?) that all entries that import at least one theory from
HOL-Library are based on HOL-Library.
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
