[isabelle] Questions about Quickcheck


I am wondering about the following things w.r.t. Quickcheck:

â 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.

â Why does quickcheck not fall back to random testing when exhaustive testing is not available?

â Why is Quickcheck for multisets only set up for random and full_exhaustive, but not for exhaustive?

â 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)


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