# Unique-functions

The condition in which all the function 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 functions;
the uniqueness property for variables
is captured in unique-variables.
We formalize this property via ACL2 functions on statements, blocks, etc.
that take as arguments the function names encountered so far,
check that the names of the functions
introduced by the statement (or block etc.)
are not among those,
and update the set of encountered function names
with the names of the introduced functions.
Thus, the set of function 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 functions.

### Subtopics

- Statements/blocks/cases/fundefs-unique-funs
- Mutually recursive functions that check
the uniqueness of function names in
statements, blocks, cases, and function definitions.