Counting in lists #
This file proves basic properties of List.countP and List.count, which count the number of
elements of a list satisfying a predicate and equal to a given element respectively. Their
definitions can be found in Batteries.Data.List.Basic.
count #
theorem
List.count_singleton'
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
:
List.count a [b] = if b = a then 1 else 0
theorem
List.count_concat
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:
List.count a (l.concat a) = (List.count a l).succ
@[deprecated List.filter_eq]
theorem
List.filter_eq'
{α : Type u_1}
[DecidableEq α]
(l : List α)
(a : α)
:
List.filter (fun (x : α) => decide (a = x)) l = List.replicate (List.count a l) a
@[deprecated List.filter_beq]
theorem
List.filter_beq'
{α : Type u_1}
[DecidableEq α]
(l : List α)
(a : α)
:
List.filter (fun (x : α) => a == x) l = List.replicate (List.count a l) a