Lemmas about List.countP
and List.count
. #
Because we mark countP_eq_length_filter
and count_eq_countP
with @[grind _=_]
,
we don't need many other @[grind]
annotations here.
countP #
@[simp]
List.countP
and List.count
. #Because we mark countP_eq_length_filter
and count_eq_countP
with @[grind _=_]
,
we don't need many other @[grind]
annotations here.