def internal_foldl_assoc
bend-mathlib@0.8.1.0 · algebra.bend:261
import bend-mathlib@0.8.1.0/algebra.bend as Algebra
import Base
261def internal_foldl_assoc(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, +xs: List<&2, B>, +a: B, +b: B) -> {List.foldl(&2, B, B, op, xs, op(a, b)) == op(a, List.foldl(&2, B, B, op, xs, b)) : B}:
262 match xs:
263 case Nil{}:
264 {==}
265 case +h <> +t:
266 %Equal.sym(B, op(op(a, b), h), op(a, op(b, h)), assoc(a, b, h)) : {List.foldl(&2, B, B, op, t, _) == op(a, List.foldl(&2, B, B, op, t, op(b, h))) : B}
267 internal_foldl_assoc(~B, ~op, ~assoc, t, a, op(b, h))