Tree.reduce_foldr: law of bend-lawful-stdlib@0.1.0.0
Import: import bend-lawful-stdlib@0.1.0.0/src/tree.bend as Tree
Lines 50-58 of bend-lawful-stdlib@0.1.0.0/src/tree.bend: https://jend.leeeet.dev/read.txt?path=bend-lawful-stdlib@0.1.0.0/src/tree.bend&start_line=50&end_line=58

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

# reduce agrees with foldr. With acc = Nil{}:
# {op(reduce(t), z) == foldr(to_list(t), z)}.
law reduce_foldr:
  for ~A: Data
  for ~m: C.Semigroup<A>
  for t: Tree<A>
  for +acc: List<&2, A>
  for +z: A
  {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}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.foldr
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup.assoc
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup.fn
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/class.bend&name=Semigroup.op
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/tree.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/tree.bend&name=reduce
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/tree.bend&name=to_list.go