law foldl_append

bend-mathlib@0.8.1.0 · list.bend:496

import Base

496# A left fold over an append folds the second part from the fold of the first.
497law foldl_append:
498  for ~a: Quant
499  for ~A: Kind(a)
500  for ~B: Type
501  for ~f: B -> A -> B
502  for xs: List<a, A>
503  for -ys: List<a, A>
504  for -z: B
505  {List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) : B}