Eta-reduction is the process of removing redundant lambda abstractions from a term. For example, the term λx. f x can be eta-reduced to f but only if
x is not free in f
f is a pure expression
Purity checking is handled by TermAnalysis.isPure. A term is pure if it does not contain any side effects, such as Error, Force of non-delayed terms, or saturated builtin applications. See TermAnalysis.isPure for comprehensive documentation on purity semantics.