aconv : term -> term -> bool

- STRUCTURE
- SYNOPSIS
- Tests for alpha-convertibility of terms.
- DESCRIPTION
- When applied to two terms, aconv returns true if they are alpha-convertible, and false otherwise. Two terms are alpha-convertible if they differ only in the way that names have been given to bound variables.
- FAILURE
- Never fails.
- EXAMPLE
- aconv (Term `?x y. x /\ y`) (Term `?y x. y /\ x`) > val it = true : bool

- SEEALSO

HOL Kananaskis-14