\subsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
β-reduction and function inlining below, all function-typed expressions should
be lambda abstractions or global identifiers.
\subsection{η-abstraction}
This transformation makes sure that all arguments of a function-typed
expression are named, by introducing lambda expressions. When combined with
β-reduction and function inlining below, all function-typed expressions should
be lambda abstractions or global identifiers.