doc: demote repeated H1 headers#36833
doc: demote repeated H1 headers#36833harahu wants to merge 2 commits intoleanprover-community:masterfrom
Conversation
PR summary 35bf175a46Import 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
|
vihdzp
left a comment
vihdzp
left a comment
There was a problem hiding this comment.
This all seems reasonable to me, as it matches what we do on most files. Perhaps we should document this somewhere? "Use H1 at the very beginning of the module docstring, use H2 afterwards within the module docstring, use H3-H6 elsewhere"
|
The style guide already more-or-less enforces this pattern:
and
It isn't really clear on why this pattern is desirable, though, which one might want to do something about. |
harahu
force-pushed
the
doc/headers-demotion-032026
branch
from
a1c10b8 to
be6ec2a
Compare
3 participants
Having more than one H1 header per file confuses search engines and thus makes documentation more difficult to find. Hence, we make sure that lean files only have a single H1 header in them.
In the case of
Mathlib/Tactic/Common.lean, we achieve this by adding a new module header.