List.filter with Bool

Stream: lean4

[Horatiu Cheval]

I just realized the following change. In Lean3:

#check @list.filter
-- list.filter : Π {α : Type u_1} (p : α → Prop) [_inst_1 : decidable_pred p], list α → list α

In Lean4:

#check @List.filter
-- List.filter : {α : Type u_1} → (α → Bool) → List α → List α

What's the reason for this change in filter?Is there a larger design decision of moving away from decidable propositions and closer to booleans? (of course the two were pretty much interchangeable in Lean3 also, due to coercions)

[Chris B]

This coercion was added to Mathlib4 to deal with the filter thing:

instance Decidable.predToBool {α : Type u} (p : α → Prop) [DecidablePred p] : CoeDep (α → Prop) p (α → Bool) where
  coe := fun b => decide $ p b

I originally thought this had to do with the addition of bool reduction to the kernel, but Mario informed me there's probably no difference in generated code between bool and a decidable prop. If I had to guess, it has to do with bool being more familiar to programmers, and making it a boolean predicate doesn't take the user's ability to write a prop-valued version and prove that p <-> (b = true), or for predicates forall x, p x <-> (b x = true). I would be interested to hear from the devs though.