doc lint on `let rec`?

Stream: mathlib4

[Kyle Miller]

The documentation linter complained about a let rec not having documentation in one of my PRs -- is this something that can be disabled in general? For one, the let rec syntax doesn't support docstrings, and for another a let rec is meant to be a local definition like any other let, so it's not clear it needs a docstring just because it's recursive.

Similarly, definitions in where clauses are flagged by the linter. Often documentation helps with these (and these do support docstrings) but I'm not sure local definitions should be required to have them.

[Alex J. Best]

I dont know that these are tagged in any way in the environment, so the only way I can think to detect them is checking if the declaration range of a def of the form a.b is contained in that of a, which is quite a hack

[Mario Carneiro]

For one, the let rec syntax doesn't support docstrings,

Actually it does, the syntax for it is just really awkward

example : True :=
  let rec /-- why is the docstring here? -/ foo : Nat := 1
  trivial

[Mario Carneiro]

it does actually make a tiny bit of sense, because a let rec can introduce multiple mutual definitions separated by commas, and they all need a docstring (and let rec introduces the whole block)

example : True :=
  let rec
    /-- I have no idea how to indent this -/
    foo : Nat := 1,
    /-- also a definition -/
    bar : Nat := foo
  trivial

[Mario Carneiro]

TBH the usage of commas here is not very lean-ish, usually you would expect the commas to be optional with whitespace-sensitivity being the alternate syntax but here there is no alternate

[Mario Carneiro]

But Alex is right, the main reason these aren't special cased is because they are not obviously different from regular definitions (assuming you are talking about the std/mathlib doc linter)

[Kevin Buzzard]

Mario Carneiro said:

it does actually make a tiny bit of sense, because a let rec can introduce multiple mutual definitions separated by commas, and they all need a docstring (and let rec introduces the whole block)

example : True :=
  let rec
    /-- I have no idea how to indent this -/
    foo : Nat := 1,
    /-- also a definition -/
    bar : Nat := foo
  trivial

Don't forget the comma!