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

add: Table of Contents to each chapter (2-12) using mdbook-toc #128

Open
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

thelissimus
Copy link

It is quite difficult to navigate back and forth without the table of contents, considering that the book is written in 12 big one-page chapters.

This PR uses mdbook-toc to generate TOC. The reason of using it is to prevent writing TOC manually - to prevent the chapter names and TOCs getting out of sync. It is added to both GitHub Pages and Netlify deployment pipeline environments. If mdbook-toc dependency is redundant the PR can be re-worked to remove mdbook-toc and add TOCs manually.

Only the GitHub Pages deployment pipeline tested (due to having no access to leanprover Netlify) and it is working perfectly. The demo deployment is available at: https://thelissimus.github.io/theorem_proving_in_lean4/

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant