chore(*): small docstring syntax fixes#38157
chore(*): small docstring syntax fixes#38157Vierkantor wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
This PR goes through and corrects all the warnings raised by `linter.style.docStringVerso` that are unrelated to LaTeX or link syntax. In addition to putting backticks around some expressions, there are a few typos (such as mismatched brackets, or syntax in the wrong order), a few unusual usages of punctuation (such as putting `{}` around names in references), and a few usages made consistent (`*`-ring, C⋆-algebra).
PR summary 4fceb4697eImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
| When a (nonunital, non-associative) semiring is equipped with an involutive automorphism the | ||
| center of the centroid becomes a star ring in a natural way and the natural mapping of the centre of | ||
| the semiring into the centre of the centroid becomes a *-homomorphism. | ||
| the semiring into the centre of the centroid becomes a `*`-homomorphism. |
There was a problem hiding this comment.
Just as with the AB axioms... What is the correct way to write an asterisk in markdown / verso? Does escaping work?
| the semiring into the centre of the centroid becomes a `*`-homomorphism. | |
| the semiring into the centre of the centroid becomes a \*-homomorphism. |
Idem dito for many other places.
There was a problem hiding this comment.
According to grep, we have about twice as many `*`-objects (39) in docstrings compared to *-objects (22). But indeed we could switch over to \*-objects, since both Markdown (CommonMark) and Verso allow backslash-escaping *.
Some more datapoints: looks like Wikipedia writes them as *-objects and the nLab writes them as $*$-objects.
I suppose \*-objects render the most naturally, so let's go for that.
|
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
This PR goes through and corrects all the warnings raised by
linter.style.docStringVersothat are unrelated to LaTeX or link syntax. In addition to putting backticks around some expressions, there are a few typos (such as mismatched brackets, or syntax in the wrong order), a few unusual usages of punctuation (such as putting{}around names in references), and a few usages made consistent (*-ring, C⋆-algebra).