argument order in`count_cons_of_ne`

Stream: lean4

[Jovan Gerbscheid]

count_cons_of_ne (h : a ≠ b) (l : List α) : count a (b :: l) = count a l

I think that a and b should be swapped in h. This is because of the convention is to put the "more variable" argument on the left, in this case b is the more variable argument.

I ran into this because I was following this convention, and the simp lemma didn't apply.

[Eric Wieser]

My initial reaction is that the order there is correct with a hypothetical "keep things in a consistent order through the statement" rule.

[Jovan Gerbscheid]

Well, it can also be stated as

theorem count_cons_of_ne (h : a ≠ b) (l : List α) : (b :: l).count a = l.count a := sorry

which would give the opposite order with that rule.

[Jovan Gerbscheid]

The thing is that the definition of List.count does follow the "more variable of the left" convention.

def count [BEq α] (a : α) : List α → Nat := countP (· == a)

So I think it's weird that this lemma flips the equality around.

[Kim Morrison]

I'd merge such a PR.

[Jovan Gerbscheid]

lean#7650

[Kim Morrison]

If you want to fix the lean-pr-testing-7650 branch at Batteries that would be great, but it's probably easy for me to do when the nightly lands.

[Jovan Gerbscheid]

I won't have time for it today