Skip to content

Replace all lemmas with markdown-generated content pages#188

Merged
ScriptRaccoon merged 2 commits into
mainfrom
replace-lemmas-with-content-pages
May 17, 2026
Merged

Replace all lemmas with markdown-generated content pages#188
ScriptRaccoon merged 2 commits into
mainfrom
replace-lemmas-with-content-pages

Conversation

@ScriptRaccoon
Copy link
Copy Markdown
Owner

@ScriptRaccoon ScriptRaccoon commented May 17, 2026

This continues #184 and replaces all lemmas with markdown-generated content pages. Together with that PR, it resolves #176. There is now a single way to author long-form content.

Accordingly, the lemmas table has been removed from the database. It was unnecessary to define lemmas in YAML files, seed them into the SQLite database, and then query them again during prerendering. The rendering is now more direct. In addition, lemmas had no relationships to other tables anyway.

before, this only rendered inline text.
@ScriptRaccoon ScriptRaccoon merged commit f1f2fcd into main May 17, 2026
1 check passed
@ScriptRaccoon ScriptRaccoon deleted the replace-lemmas-with-content-pages branch May 17, 2026 11:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Unify lemmas, pdfs, and long proofs

1 participant