changing names in ForIn docs

Stream: lean4

[Alok Singh]

Naming the arguments in only greek letters just seems a bit perverse. \rho instead of 'seq' or something.

I propose that we change it and am happy to implement it.

[Eric Wieser]

Looking at docs#ForIn, I'm very puzzled by how [inst : Monad m] is quantified over in ForIn.forIn; surely we don't want to quantify over all non-canonical monad structures on m? Shouldn't [Monad m] be a parameter on the typeclass instead?

[Mario Carneiro]

I don't think it makes much of a difference. A ForIn impl is supposed to be parametric over the monad anyway

[Mario Carneiro]

But it's true that it is a bit weird that m is a parameter but Monad m is an argument to the forIn function