[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