Feature request: docstrings for instance fields

Stream: lean4

[James Gallicchio]

Hey, thinking about documentation for Std collections, and I'm wondering if anyone has thoughts about attaching doc-strings to an instance's fields, to show to users when that field is accessed. For example:

/-- Class for undirected `fold`. -/
class Fold (C) (τ : outParam _) where
  /-- undirected `fold` consumes one element at a time in a collection. -/
  fold : {β : Type w} → (β → τ → β) → β → C → β

/-- Fold for lists; defeq to `foldl`, chosen over `foldr` because
`foldl` is tail-recursive.
-/
instance : Fold (List τ) τ where
  /-- Implemented as a left fold; O(n). -/
  fold := List.foldl

#check (Fold.fold : _ → _ → List Nat → Nat)

It would be suuuuper cool if hovering over the Fold.fold at #check showed the "instance docstring" in addition to the class docstring for that field.

[James Gallicchio]

The reason I'm asking is that I would like collection operation complexities to be relatively visible, but operation complexity varies wildly between implementations.

If collection operations are accessed by users via typeclasses (which I expect they will be) then there's not a great way to expose that info to users...

[Henrik Böving]

So right now documentation is attached to actual declaratoins in the Environment and the fold in the instance isn't a declaration in the Environment I think? So this feature is definitley not missing just because someone was lazy you would have to put actual work into it.

[Wojciech Nawrocki]

Related: https://github.com/leanprover/lean4/pull/1767

[James Gallicchio]

That is a big PR :sweat_smile: what is the current status of it?

[Wojciech Nawrocki]

I think it's just waiting to be merged modulo some CI errors