1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\DOC genvar
\TYPE {genvar : hol_type -> term}
\SYNOPSIS
Returns a `fresh' variable with specified type.
\DESCRIBE
When given a type, {genvar} returns a variable of that type whose name has not
previously been produced by {genvar}.
\FAILURE
Never fails.
\EXAMPLE
The following indicates the typical stylized form of the names (this should
not be relied on, of course):
{
# genvar `:bool`;;
val it : term = `_56799`
}
There is no guard against users' own variables clashing, but if the user avoids
names in the same lexical style, that can be guaranteed.
\USES
The unique variables are useful in writing derived rules, for specializing
terms without having to worry about such things as free variable capture.
If the names are to be visible to a typical user, the function {variant} can
provide rather more meaningful names.
\SEEALSO
variant.
\ENDDOC
|
