Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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%%763)”, “$var$(%%genvar%%764)”, “$var$(%%genvar%%765)”]:
   term list

See also

Term.genvar, Term.mk_var