allow adding doctring to standalone deriving

Stream: lean4

[Alok Singh]

The following is legal, so allowing attaching docs to the standalone deriving clause seems legit

-- To allow printing Lean.NameSet and Std.HashMap for `transitivelyUsedConstants`
deriving instance Repr for Lean.NameSet
deriving instance Repr for Std.HashMap
deriving instance Hashable for Substring
deriving instance Hashable for SourceInfo
deriving instance Hashable for Syntax.Preresolved
deriving instance Hashable for Syntax
/-- Make `Syntax` hashable for `matchOnTree` to put in `HashSet` later-/
instance : Hashable Syntax where
  hash := fun syn => Hashable.hash syn

The final manual instance is only needed to get the docstring.

[Kim Morrison]

You could use add_decl_doc in the meantime. Seems a reasonable RFC to allow docstrings on standalone deriving, I agree. Do you want to write it?

[Alok Singh]

https://github.com/leanprover/lean4/issues/6896#issue-2824788810

[Kim Morrison]

@Alok Singh, this RFC is inadequate: you don't even state what you want to change, just give an example. We can work it out from the example, but it's not really what we're hoping for from RFCs.

[Kyle Miller]

Question: what happens if you do deriving instance Repr for Type1, Type2 with a docstring?