RFC: add the option to add a prefix and a suffix to a doc-string when using inherit_doc

[adomani]

Proposal

Currently, @[inherit_doc foo] def bar ... copies the doc-string of foo to bar.

The proposal is to add the option of extending the docs of foo by prefixing and suffixing extra strings.

Here is a sample usage

/-- `foo` is `1` -/
def foo : ℕ := 1

@[inherit_doc foo
  before "`fooPlusOne` looks like `foo`:"
  after "... except that it adds one to it."]
def fooPlusOne : ℕ := foo + 1

#check fooPlusOne
-- hover over `fooPlusOne` shows
/-
`fooPlusOne` looks like `foo`:

`foo` is 1

... except that it adds one to it.
-/

• User Experience: This allows to copy over docs from "parent" declarations and highlight how children differ from their parents.

• Beneficiaries: The proposal arose from discussions in Mathlib. Relevant Zulip thread.

• Maintainability: I have no expertise in answering this question, but my naive impression is that it would not require much maintenance.

Community Feedback

The Zulip thread mentioned above originated from the current doc-string for rw, which mentions rewrite but not what rw actually does.

With the current proposal, the docs for rw could be inherited from rewrite, preceded with the sentence that is currently the doc-string for rw.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[semorrison]

@adomani, I don't think this belongs in core. Is there any reason it can't go in Std?

[adomani]

@semorrison, I was simply going by what I thought that Mario had suggested in the Zulip chat. I do not mind if it goes in Std or core, though.

[digama0]

@semorrison Yes, this has to be implemented in core, because inherit_doc is specifically handled by some other definitions like notation. If you try to implement a copy of inherit_doc with additional syntax and behavior (as Damiano did), you get errors when using it with notation in the same way as inherit_doc. To fix this you would have to replace notation, which will cause more knock on effects requiring even more replacements.