rename_bvar
Term.rename_bvar : string -> term -> term
Performs one step of alpha conversion.
If M is a lambda abstraction, i.e., has the form \v.N, an invocation
rename_bvar s M performs one step of alpha conversion to obtain
\s. N[s/v].
Failure
If M is not a lambda abstraction.
Example
> rename_bvar "x" (Term `\v. v ==> w`);
val it = “λx. x ⇒ w”: term
> rename_bvar "x" (Term `\y. y /\ x`);
val it = “λx'. x' ∧ x”: term
Comments
rename_bvar takes constant time in the current implementation.