Documentation

manifestArity sees how many leading value lambdas there are, after looking through casts

An approximate, fast, version of exprEtaExpandArity

The Arity returned is the number of value args the expression can be applied to without doing much work

etaExpand n e returns an expression with the same meaning as e, but with arity n.

Given:

e' = etaExpand n e

We should have that:

ty = exprType e = exprType e'

Split an expression into the given number of binders and a body, eta-expanding if necessary. Counts value *and* type binders.