law filter_true_sym

bend-mathlib@0.8.1.0 · list.bend:2737

import Base

2737# Filtering with an always-true predicate gives the list back, reversed to rewrite toward the simple side.
2738law filter_true_sym:
2739  for ~A: Data
2740  for xs: List<&2, A>
2741  {xs == List.filter(~A, ~(x => True{}), xs) : List<&2, A>}