feat: add @[inheritDoc] attribute

[digama0]

• depends on feat: attributes on notation #1478
• depends on feat: attributes on {macro,elab}(_rules) #1483

This attribute allows you to specify another declaration to copy the docstring for the given declaration from. Example:

/-- Foo doc string -/ def foo := 1
@[inheritDoc foo] def bar := 1

This will give bar the same docstring as foo. It does not otherwise link the two declarations, but users that arrive at bar can click on the foo identifier to jump to the other declaration.

For infix and notation declarations, it is also possible to omit the identifier, in which case it will use the declaration the notation unfolds to. For example:

@[inheritDoc] infix:65 " >+< " => Nat.add

This gives the >+< syntax the same docstring as Nat.add.

@[inheritDoc] is also integrated into the missingDocs linter, which will not lint on declarations which have @[inheritDoc] but no documentation.