rename_bvar : string -> term -> term

- STRUCTURE
- SYNOPSIS
- Performs one step of alpha conversion.
- DESCRIPTION
- 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.
- SEEALSO

HOL Kananaskis-14