/usr/share/hol88-2.02.19940316/help/ENTRIES/variant.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 43 44 45 46 | \DOC variant
\TYPE {variant : (term list -> term -> term)}
\SYNOPSIS
Modifies a variable name to avoid clashes.
\DESCRIBE
When applied to a list of variables to avoid clashing with, and a variable to
modify, {variant} returns a variant of the variable to modify, that is, it
changes the name as intuitively as possible to make it distinct from any
variables in the list, or any (non-hidden) constants. This is normally done by
adding primes to the name.
The exact form of the variable name should not be relied on, except that the
original variable will be returned unmodified unless it is itself in the list
to avoid clashing with.
\FAILURE
{variant l t} fails if any term in the list {l} is not a variable or if
{t} is neither a variable nor a constant.
\EXAMPLE
The following shows a couple of typical cases:
{
#variant ["y:bool"; "z:bool"] "x:bool";;
"x" : term
#variant ["x:bool"; "x':num"; "x'':num"] "x:bool";;
"x'''" : term
}
\noindent while the following shows that clashes with the names of constants
are also avoided:
{
#variant [] (mk_var(`T`,":bool"));;
"T'" : term
}
\USES
The function {variant} is extremely useful for complicated derived rules which
need to rename variables to avoid free variable capture while still making the
role of the variable obvious to the user.
\SEEALSO
genvar, hide_constant.
\ENDDOC
|