Re: [isabelle] Questions about Quickcheck

Hi Manuel,

â What is the real difference between exhaustive and full_exhaustive? There are a sentence
or two on this in isar-ref about term reconstruction, but it's not quite clear to me what
that actually means.

AFAIK exchaustive and full_exhaustive are two different compilation schemes, but I don't know
the details. You can switch between the two schemes with the option quickcheck_full_support.
Since this option is enabled by default, the exhaustive tester is essentially untested.
Most types in the library do not have any setup for exhaustive any more (in particular all the datatypes, it seems).

â Is there any reason not to simply replace the entire Quickcheck setup for multisets with
"quickcheck_generator multiset construtors: mset"? (I have done that locally and it seems
to work well)
AFAICS, you get essentially the same testers.


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