Skip to content

fix: close module doc blocks in Section_3_2 and Section_3_5#592

Merged
teorth merged 1 commit into
teorth:mainfrom
Chessing234:fix/module-doc-closers-3-2-3-5
Jul 17, 2026
Merged

fix: close module doc blocks in Section_3_2 and Section_3_5#592
teorth merged 1 commit into
teorth:mainfrom
Chessing234:fix/module-doc-closers-3-2-3-5

Conversation

@Chessing234

Copy link
Copy Markdown
Contributor

Summary

  • Section_3_2.lean and Section_3_5.lean opened /-! module docs but closed with --/.
  • Corrected to -/ so Verso can parse the section headers.

Test plan

  • CI Build book

Made with Cursor

/-! headers were closed with --/ instead of -/.

Co-authored-by: Cursor <cursoragent@cursor.com>
@teorth
teorth merged commit bb62034 into teorth:main Jul 17, 2026
2 checks passed
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.

2 participants