# Unique-variables

The condition in which all the variable names are distinct.

The Disambiguator transformation described in
[Solidity: Internals: The Optimizer: Yul-Based Optimizer Module:
Preprocessing: Disambiguator],
makes all the variable and function names globally unique.

Here we capture this uniqueness property for variables;
the uniqueness property for functions
is captured in unique-functions.
We formalize this property via ACL2 functions on statements, blocks, etc.
that take as arguments the variable names encountered so far,
check that the names of the variables
introduced by the statement (or block etc.)
are not among those,
and update the set of encountered variable names
with the names of the introduced variables.
Thus, the set of variable names encountered so far is threaded through.
We do not need to define any ACL2 functions on expressions,
in order to capture this property,
because expressions do not introduce new variables.

### Subtopics

- Statements/blocks/cases/fundefs-unique-vars
- Mutually recursive functions that check
the uniqueness of variable names in
statements, blocks, cases, and function definitions.
- Var-unique-vars
- Check that a variable is unique.
- Var-list-unique-vars
- Check that all the variables in a list are unique.
- Statements/blocks/cases/fundefs-unique-vars-extend
- The ...-unique-vars functions extend the set of variables.