Commit 2022-10-04 05:52 561202d0
View on Github →refactor(data/list/count): review API, add lemmas (#16736)
- add
list.countp_join
,list.countp_map
,list.countp_mono_left
,list.countp_congr
, andlist.count_join
; - add
@[simp]
attrs tolist.countp_eq_zero
,list.countp_eq_length
,list.count_eq_zero
, andlist.count_eq_length
; - golf the proofs of
list.count_bind
,list.count_map_of_injective
, andlist.count_le_count_map
.