law filter_append

bend-mathlib@0.8.1.0 · list.bend:647

import Base

647# Filtering an append filters each part.
648law filter_append:
649  for ~A: Data
650  for ~f: A -> Bool
651  for xs: List<&2, A>
652  for ys: List<&2, A>
653  {List.filter(~A, ~f, List.append(&2, A, xs, ys)) == List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) : List<&2, A>}