Convention for implicit arguments

Stream: mathlib4

[Chris Wong]

@Yaël Dillies brought up a guideline for when to use implicit arguments:
https://github.com/leanprover-community/mathlib4/pull/11311#discussion_r1905383279

Do we have a discussion thread for this guideline? And can we add it to the style guide?

I ask because I'm adding "reversal of regular languages" to the NFA module, and I want to decide whether I should align the existing lemmas with the guideline first.

[Yaël Dillies]

I'm currently writing a full guide on argument implicitness. But it's going slowly because I have other obligations

[Kim Morrison]

@Yaël Dillies, I would love to have this, codifying it would be really helpful. I'd be interested in trying to turn as much as possible in an (optional) linter, too.

[Yaël Dillies]

That would be great! In fact, I am hoping we can turn both the implicitness convention and the symbol-reading naming convention into interactive games that people can play to learn them

[Yaël Dillies]

(this is too ambitious to even be on my todo list, though)

[Kim Morrison]

We'd like to write down conventions for implicit arguments for the Lean repo, too, see WIP at https://github.com/leanprover/lean4/pull/6974/files#diff-6b7681f195d5ac6e0c00f239b5d9cc36c2f74a4773377c070765d2d9bec9332cR8.

@Yaël Dillies, if you're able to write something too this will really help in aligning these conventions.

[Kim Morrison]

(I think we are still thinking "need to do some research" to get the answer right here, and are very happy to have inspiration!)

[Yaël Dillies]

Right, okay. I will bump that up my TODO list!