law foldl_eq_foldr

bend-mathlib@0.8.1.0 · algebra.bend:279

import Base

279# Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr).
280law foldl_eq_foldr:
281  for ~B: Data
282  for ~op: B -> B -> B
283  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
284  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
285  for +z: B
286  for +xs: List<&2, B>
287  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}