[Merged by Bors] - chore(Algebra/FreeAlgebra): fix ported comments

[utensil]

Per discussion on zulip.

---

The comments were ported from mathlib 3, but turned into semantically incorrect comments, this PR recovers the original semantics.

[eric-wieser]

bors merge

Thanks! Can you look for other occurrences of \w--? I would guess that all line comments with no preceding whitespace are mathport errors.

[utensil]

Can you look for other occurrences of \w--? I would guess that all line comments with no preceding whitespace are mathport errors.

Yes, I have run a search of inductive in Mathlib, gone through the 5 pages, and it seems to be the only case that matters:

• most inductive types don't have comments inside them
• most that have are for tactics and well written with /-- -/ which are properly rendered in doc-gen4, e.g. Mathlib.Explode.Status
• The only case that uses -- inside inductive is Algebra.Category.MonCat.Colimits.Prequotient where the comments are well formated

It's safe to say that this is an edge case that has minimal impact.

EDIT: local search with variants of \w\ -- \w+\n found nothing suspicious too.

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style