Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-02 04:55 309df10a

View on Github →

refactor(data/list/basic,...): more explicit args (#4866) This makes the p in most lemmas involving the following functions explicit, following the usual explicitness conventions:

  • list.filter,
  • list.countp,
  • list.take_while,
  • multiset.filter,
  • multiset.countp,
  • finset.filter

Estimated changes

modified def finset.filter
modified theorem finset.filter_empty
modified theorem finset.filter_filter
modified theorem finset.filter_inter
modified theorem finset.filter_subset
modified theorem finset.filter_union
modified theorem finset.filter_union_right
modified theorem finset.inter_filter
modified theorem list.countp_nil
modified theorem list.filter_filter
modified theorem list.span_eq_take_drop
modified theorem list.take_while_append_drop
modified theorem multiset.coe_count
modified theorem multiset.coe_filter
modified def multiset.countp
modified theorem multiset.countp_filter
modified theorem multiset.countp_zero
modified def multiset.filter
modified theorem multiset.filter_add
modified theorem multiset.filter_add_filter
modified theorem multiset.filter_filter
modified theorem multiset.filter_map_filter
modified theorem multiset.filter_zero