# [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.*