EtaReduce

Performs eta-reduction on a term.

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.