Linter complains about `let rec` missing docstring

Stream: mathlib4

[Alex Keizer]

While porting data.fintype.option, I replaced an inductive' tactic with an explicit structural recursion to maintain computability.

/-- A recursor principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`. -/
def truncRecEmptyOption {P : Type u → Sort v} (of_equiv : ∀ {α β}, α ≃ β → P α → P β)
    (h_empty : P PEmpty) (h_option : ∀ {α} [Fintype α] [DecidableEq α], P α → P (Option α))
    (α : Type u) [Fintype α] [DecidableEq α] : Trunc (P α) := by
  suffices ∀ n : ℕ, Trunc (P (ULift <| Fin n))
    by sorry
  -- porting note: do a manual recursion, instead of `induction` tactic,
  -- to ensure the result is computable
  let rec ind : ∀ n : ℕ, Trunc (P (ULift <| Fin n))
  | Nat.zero => by sorry
  | Nat.succ n => by sorry
  apply ind

The lint complains that ind is missing a docstring

DEFINITIONS ARE MISSING DOCUMENTATION STRINGS: -/
-- Mathlib.Data.Fintype.Option
#check Fintype.truncRecEmptyOption.ind.{u, v} /- definition missing documentation string -/

But, I cannot attach a docstring to a let rec binding, it complains that a declaration was expected.

[Johan Commelin]

For now, just add a -- Porting note and a attribute [nolint], I guess?

[Alex Keizer]

I forgot about nolint, thanks for the suggestion

[Alex Keizer]

Ah, that doesn't work. It seems the nolint only applies to the original definition, but the auxiliary truncRecEmptyOption.ind definition is still being complained about.
I'll go for plan B, explicitly moving ind to a separate definition, rather than relying on let rec

[Johan Commelin]

Does it work to write

attribute [nolint SomeLinterName] truncRecEmptyOption.ind

after the defn?

[Alex Keizer]

Yes, that did the trick!

[Damiano Testa]

Would something along these lines work as well?

/-- doc string for `f`. -/
def f : Nat → Nat := by
  apply newDef where
    /--  I am a docstring -/
    newDef := Nat.succ

#eval f 3
#check f.newDef -- hover over me

[Alex Keizer]

Yes, that one works as well, and is probably a bit cleaner

[Damiano Testa]

Ok, I am happy to know that this would have worked: I found the syntax cool and was hoping that it would work in such situations!