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