Lean4
/-- `sumList prepOp left_assoc? exs` assumes that `prepOp` is an `Expr`ession representing a
binary operation already fully applied up until its last two arguments and assumes that the
last two arguments are the operands of the operation.
Such an expression is the result of `prepareOp`.
If `exs` is the list `[e₁, e₂, ..., eₙ]` of `Expr`essions, then `sumList prepOp left_assoc? exs`
returns
* `prepOp (prepOp( ... prepOp (prepOp e₁ e₂) e₃) ... eₙ)`, if `left_assoc?` is `false`, and
* `prepOp e₁ (prepOp e₂ (... prepOp (prepOp eₙ₋₁ eₙ))`, if `left_assoc?` is `true`.
-/
partial def sumList (prepOp : Expr) (left_assoc? : Bool) : List Expr → Expr
| [] => default
| [a] => a
| a :: as =>
if left_assoc? then Expr.app (prepOp.app a) (sumList prepOp true as)
else as.foldl (fun x y => Expr.app (prepOp.app x) y) a
