law filter_false

bend-mathlib@0.8.1.0 · list.bend:1404

import Base

1404# Filtering with an always-false predicate gives the empty list.
1405law filter_false:
1406  for ~A: Data
1407  for xs: List<&2, A>
1408  {List.filter(~A, ~(x => False{}), xs) == Nil{} : List<&2, A>}