[isabelle] Random term given its type
Is there a function in Isabelle/ML to generate a random term of a given a
type (and potentially instantiate type vars).
val random_term : int -> typ -> term
where the first parameter is a seed and the second is the type of the
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
Dr. Omar MontaÃo Rivas
e-mail: omar.montano at upslp.edu.mx
Tel. +52 (444) 8126367 ext. 225
This archive was generated by a fusion of
Pipermail (Mailman edition) and