Improve handling of inner docstring comments

[jaybosamiya-ms]

This PR fixes #102.

At a high level, this PR stops treating ///-prefixed docstring comments as comments, but as a syntactic structure of their own.

In essence, docstrings can only be used wherever an attr can be used (it might even be a subset of those cases, but handling it wherever attributes are handled should handle all important cases, since /// docstring comments are essentially syntax sugar for the #[doc(...)] attribute).

By removing it from normal comment handling, we gain more control over them, and can actually place them correctly, touching the actual code they should be touching; also we don't need to perform any of the normal comment management/manipulation code on them, since they are already all in place.

This PR does cause some minor churn around a small handful of docstring comments in our snapshotted files (see the second commit in this PR), but reading through all of them, it seems largely either acceptable, or even welcome changes (e.g., making the docstring associate with the next item, rather than with the previous item).

[jaybosamiya-ms]

Note to self: due to changing files in the snapshots, we should increment the minor version number, rather than patch, when we release this. Also, this will need a corresponding vstd PR.

[parno]

This looks reasonable to me. Thanks for the helpful comments in verus.pest. I agree that the minor changes to the snapshots seem positive or at worst neutral, so this seems like a good change.