Returns a pair structure of variables whose names have not been previously used.
DESCRIPTION
When given a product type, genvarstruct returns a
paired structure of variables whose names have not been
used for variables or constants in the HOL session so far.
The structure of the term returned will be identical to the structure of the
argument.
FAILURE
Never fails.
EXAMPLE
The following example illustrates the behaviour of genvarstruct:
- genvarstruct (type_of (Term `((1,2),(x:'a,x:'a))`));
> val it = `((%%genvar%%1535,%%genvar%%1536),%%genvar%%1537,%%genvar%%1538)`
: term
USES
Unique variables are useful in writing derived rules, for specializing
terms without having to worry about such things as free variable capture.
It is often important in such rules to keep the same structure.
If not, genvar will be adequate.
If the names are to be visible to a typical user, the function pvariant can
provide rather more meaningful names.