Lean4
/-- `prepareOp sum` takes an `Expr`ession as input. It assumes that `sum` is a well-formed
term representing a repeated application of a binary operation and that the summands are the
last two arguments passed to the operation.
It returns the expression consisting of the operation with all its arguments already applied,
except for the last two.
This is similar to `Lean.Meta.mkAdd, Lean.Meta.mkMul`, except that the resulting operation is
primed to work with operands of the same type as the ones already appearing in `sum`.
This is useful to rearrange the operands.
-/
def prepareOp (sum : Expr) : Expr :=
let opargs := sum.getAppArgs
(opargs.toList.take (opargs.size - 2)).foldl (fun x y => Expr.app x y) sum.getAppFn
