law reduce_foldr

bend-lawful-stdlib@0.1.0.0 · src/tree.bend:50

import Base
import bend-lawful-stdlib@0.1.0.0/src/class.bend as C

50# reduce agrees with foldr. With acc = Nil{}:
51# {op(reduce(t), z) == foldr(to_list(t), z)}.
52law reduce_foldr:
53  for ~A: Data
54  for ~m: C.Semigroup<A>
55  for t: Tree<A>
56  for +acc: List<&2, A>
57  for +z: A
58  {C.Semigroup.op(A, m, reduce(~A, ~m, t), List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), acc, z)) == List.foldr(~&2, ~A, ~A, ~C.Semigroup.fn(~A, ~m), to_list.go(A, t, acc), z) : A}