genvars

Term.genvars : hol_type -> int -> term list

Generate a specified number of fresh variables.

An invocation genvars ty n will invoke genvar n times and return the resulting list of variables.

Failure

Never fails. If n is less-than-or-equal to zero, the empty list is returned.

Example

> genvars alpha 3;
val it =
   [“$var$(%%genvar%%1100)”, “$var$(%%genvar%%1101)”,
    “$var$(%%genvar%%1102)”]: term list

See also

Term.genvar, Term.mk_var