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.

See also

Term.aconv, Drule.ALPHA_CONV