Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mark Planned Content with a dagger already in the section title #231

Open
nomeata opened this issue Jan 7, 2025 · 1 comment
Open

Mark Planned Content with a dagger already in the section title #231

nomeata opened this issue Jan 7, 2025 · 1 comment
Labels
doc-request Request for missing documenation

Comments

@nomeata
Copy link
Collaborator

nomeata commented Jan 7, 2025

While the manual is already in use, but incomplete, it is somewhat disappointing to hopefully click on a section title, like “Quotients”, to only then see “Planned Content”. We can maybe avoid this anti-dopamine kick for our users if all sections with Planned Content are marked as such in the TOC, for example by writing Quotiens†, in a clever pun for inaccessible names in Lean.

@nomeata nomeata added the doc-request Request for missing documenation label Jan 7, 2025
@david-christiansen
Copy link
Collaborator

Not a bad idea - but I hope that there will be no such sections quite soon, so I'm not inclined to spend a lot of time on this part.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
doc-request Request for missing documenation
Projects
None yet
Development

No branches or pull requests

2 participants