variant : term list -> term -> term
Modifies a variable name to avoid clashes.
The call variant avoid v returns a variant of v, with the name changed by
adding primes as much as necessary to avoid clashing with any free variables of
the terms in the list avoid. Usually avoid is just a list of variables, in
which case v is renamed so as to be different from all of them.
The exact form of the variable name should not be relied on, except that the
original variable will be returned unmodified unless it is free in some term in
the avoid list.
- FAILURE CONDITIONS
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.
The following shows a few typical cases:
# variant [`y:bool`; `z:bool`] `x:bool`;;
val it : term = `x`
# variant [`x:bool`; `x':num`; `x'':num`] `x:bool`;;
val it : term = `x'`
# variant [`x:bool`; `x':bool`; `x'':bool`] `x:bool`;;
val it : term = `x'''`
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.
- SEE ALSO