Implicit parameters in standard library

Stream: lean4

[Robin Arnez]

I think we should clarify exactly when to use and when not to use implicit parameters for theorems in core lean. The current convention seems to opt for more implicit parameters while older theorems often use less implicits but in general the use of implicits vs explicits is inconsistent across the codebase. Also, the issue of implicit parameters recently came up as lean4#8244. Ideally, we should get a consensus on how to approach implicits and then put it into the standard library docs.

[Markus Himmel]

Yes, a policy is in the works (possibly pending some coordination between core and mathlib). Once there is a draft I can share it here for discussion.

[Yaël Dillies]

Just adding that I've been writing a document explaining the current convention in mathlib