[isabelle] Random term given its type



Hi,

Is there a function in Isabelle/ML to generate a random term of a given a
type (and potentially instantiate type vars).

e.g.

val random_term : int -> typ -> term

where the first parameter is a seed and the second is the type of the
random term.

If not, would be difficult to use existing Quickcheck or Nitpick code to
program such function?

I was looking at the files src/HOL/Tools/Quickcheck/random_generators.ML
and exhaustive_generators.ML but I could not figure out how to use the ML
structures.

Thanks,
-- 
Dr. Omar MontaÃo Rivas
Profesor-Investigador UPSLP
e-mail: omar.montano at upslp.edu.mx
Tel. +52 (444) 8126367 ext. 225
URL: http://atit.upslp.edu.mx/index.php/omarmrivas



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