doc: Don't say "Reference implementation" in doc strings

[girving]

The docstring is for the user of the function, who doesn't need to care that it is a reference implementation. Instead, make the "reference implementation" bit a comment in the body of the reference implementation.

[digama0]

Hm, I was hoping you would put actual documentation on the functions instead...

I don't think we need this comment at all. This is implied by the use of the implemented_by attribute, and we could well say the same thing on every such attribute. More importantly, the doc is self-referential, it doesn't make sense to say that Array.foldl is the reference implementation of Array.foldl and link to itself. The more sensible thing would be to have a comment (even a doc comment) on Array.foldlUnsafe saying it is the implementation of Array.foldl.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e814fc859e8feb2c7e1c94a1d8b05e8b27149e62 --onto e6d6855a854cbde5bf7d99c7997443427dcfdba9. (2024-03-04 22:58:06)

[girving]

I'm happy to just remove the comments, but I don't want to write detailed replacement doc strings at the moment. Let me know if the former is sufficient; otherwise I can retract this one.

[kim-em]

Yeah, doesn't seem like a positive change.