def internal_foldl_eq_foldr
bend-mathlib@0.8.1.0 · algebra.bend:269
import bend-mathlib@0.8.1.0/algebra.bend as Algebra
import Base
269def internal_foldl_eq_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, +z: B, +xs: List<&2, B>) -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}:
270 match xs:
271 case Nil{}:
272 {==}
273 case +h <> +t:
274 %comm(h, z) : {List.foldl(&2, B, B, op, t, _) == op(h, List.foldr(&2, B, B, op, t, z)) : B}
275 %Equal.sym(B, List.foldl(&2, B, B, op, t, op(h, z)), op(h, List.foldl(&2, B, B, op, t, z)), internal_foldl_assoc(~B, ~op, ~assoc, t, h, z)) : {_ == op(h, List.foldr(&2, B, B, op, t, z)) : B}
276 %internal_foldl_eq_foldr(~B, ~op, ~assoc, ~comm, z, t) : {op(h, List.foldl(&2, B, B, op, t, z)) == op(h, _) : B}
277 {==}