ForIn.forIn and Monad-instance

Stream: lean4

[Alexander Bentkamp]

Hi, is there a good reason why the Monad m requirement is on ForIn.forIn rather than on the ForIn class itself? I would like to define an instance for my own monad, but I can only define it for the specific Monad instance I am using, not for an arbitrary Monad instance.

Why not define ForIn like this?

class ForIn (m : Type u₁ → Type u₂) [Monad m] (ρ : Type u) (α : outParam (Type v)) where
  forIn {β} (xs : ρ) (b : β) (f : α → β → m (ForInStep β)) : m β

[Markus Himmel]

This is going to be the changed, see lean4#10204.

[Alexander Bentkamp]

That's great. Thanks!

[Markus Himmel]

Update: this is merged now, so it will be part of Lean 4.27.0.