/usr/share/hol88-2.02.19940316/help/ENTRIES/genvar.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 35 36 37 38 39 40 41 42 | \DOC genvar
\TYPE {genvar : (type -> term)}
\SYNOPSIS
Returns a variable whose name has not been used previously.
\DESCRIBE
When given a type, {genvar} returns a variable of that type whose name has
not been used for a variable or constant in the HOL session so far.
\FAILURE
Never fails.
\EXAMPLE
The following indicates the typical stylized form of the names (this should
not be relied on, of course):
{
#genvar ":bool";;
"GEN%VAR%357" : term
#genvar ":num";;
"GEN%VAR%358" : term
}
\noindent Trying to anticipate {genvar} doesn't work:
{
#let v = mk_var(`GEN%VAR%359`,":bool");;
v = "GEN%VAR%359" : term
#genvar ":bool";;
"GEN%VAR%360" : term
}
\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
GSPEC, variant.
\ENDDOC
|