law filter_false_sym

bend-mathlib@0.8.1.0 · list.bend:2746

import Base

2746# Filtering with an always-false predicate gives the empty list, reversed to rewrite toward the simple side.
2747law filter_false_sym:
2748  for ~A: Data
2749  for xs: List<&2, A>
2750  {Nil{} == List.filter(~A, ~(x => False{}), xs) : List<&2, A>}