Re: [isabelle] Random term given its type
a few years ago, a student at the Isabelle chair in Munich wrote a
bachelor thesis, which created a property-based testing tool (based on
previous quickcheck for ML implementation). Unfortunately, I could not
found a public available link to this bachelor thesis. The source code
is however available in the directory src/Tools/Spec_Check.
Especially, the function to create a random term was implemented in
Personally, I would also suggest to experiment with an alternative
generator that exhaustively enumerates small terms.
The randomly generated terms at larger size might have a very low
probability to fulfil the conditions you are interested in. Hence,
checking all small terms might be more successful; an observation that
has led us to choose exhaustive testing for the auto quickcheck tool
This archive was generated by a fusion of
Pipermail (Mailman edition) and