Error: "invalid field 'countp', the environment...

Stream: mathlib4

[Lev Stambler]

Hello, I am trying to import "Mathlib.Probability.Independence.Basic" into a Lean file. I am getting the following error:

./lake-packages/mathlib/././Mathlib/Lean/Meta.lean:140:9: error: invalid field 'countp', the environment does not contain 'List.countp'

I am not quite sure how to go about debugging this. When I open and load Mathlib/Lean/Meta.lean, I find that the following line has an error

return (← getLocalHyps).toList.countp fun h => h.occurs e'

of invalid field 'countp', the environment does not contain 'List.countp'.

Does anyone have any idea of what to do here?

[Matthew Ballard]

countP I think

[Ruben Van de Velde]

Your versions of mathlib and std4 are not compatible. Is this in a project of your own or in mathlib?

[Scott Morrison]

countP was recently renamed