Re: [isabelle] Quickcheck ML

Hi to you all.

Le 27/06/12 10:20, Jasmin Blanchette a écrit :
Am 27.06.2012 um 09:03 schrieb Moa Johansson:

I'd like to know what the last argument of type (term * term list) list is representing? Which list is the list of terms I want to counter-example check, and what does the first term in the pair represent?

Looking at the code, it would seem that the first component is _the_ term to check and the second component is a list of terms that are additionally evaluated. For example, if you pass ("rev xs = xs", ["rev xs"]), Quickcheck will find a counterexample and print the value of "rev xs" (in addition to that of "xs"). In your use scenario, you would probably pass an empty list for the second components.

By the way, it seems that this nice feature of Quickcheck (the "eval" parameter) does not always work with the narrowing tester. This is not fully surprising since the narrowing-driven testing may send back partially instanciated values, like _#[] for instance.

However, if it is the case it may be a good idea to mention this in the isar manual.

Best regards,


Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at

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