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
|
\DOC variants
\TYPE {variants : term list -> term list -> term list}
\SYNOPSIS
Pick a list of variants of variables, avoiding a list of variables and each
other.
\DESCRIBE
The call {variants av vs},s where {av} and {vs} are both lists of variables,
will return a list {vs'} of variants of the variables in the list {vs}, renamed
as necessary by adding primes to avoid clashing with any free variables of the
terms in the list {av} or with each other.
\FAILURE
Fails if any of the terms in the list is not a variable.
\EXAMPLE
{
# variants [`x':num`; `x'':num`; `y:bool`] [`x:num`; `x':num`];;
val it : term list = [`x`; `x'''`]
}
\SEEALSO
genvar, mk_primed_var, variant.
\ENDDOC
|
