mk_primed_var : term list -> term -> term
Rename variable to avoid specified names and constant names.
The call mk_primed_var avoid v will return a renamed variant of v, by
adding primes, so that its name is not the same as any of the variables in the
list avoid, nor the same as any constant name. It is a more conservative
version of the renaming function variant.
- FAILURE CONDITIONS
Fails if one of the items in the list avoids is not a variable, or if v
itself is not.
This shows how the effect is more conservative than variant because it even
avoids variables of the same name and different type:
and this shows how it also avoids constant names:
# variant [`x:bool`] `x:num`;;
val it : term = `x`
# mk_primed_var [`x:bool`] `x:num`;;
val it : term = `x'`
# mk_primed_var  (mk_var("T",`:num`));;
val it : term = `T'`
- SEE ALSO