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