Skip to content

chore: add tests for TeX output - #545

Merged
jcreedcmu merged 4 commits into
leanprover:mainfrom
jcreedcmu:jcreed-manual-tex-unit-tests
Oct 7, 2025
Merged

chore: add tests for TeX output#545
jcreedcmu merged 4 commits into
leanprover:mainfrom
jcreedcmu:jcreed-manual-tex-unit-tests

Conversation

@jcreedcmu

@jcreedcmu jcreedcmu commented Oct 1, 2025

Copy link
Copy Markdown
Collaborator

Add a simple integration test that runs TeX generation and compares against expected output.
Also add a couple of unit tests that directly check toTex on small explicitly constructed blocks.

A continuation of the attempt in #519.

@jcreedcmu
jcreedcmu force-pushed the jcreed-manual-tex-unit-tests branch from 3fcd47c to 5fced2d Compare October 1, 2025 13:38
@jcreedcmu jcreedcmu changed the title chore: Add an integration test for TeX output chore: add tests for TeX output Oct 2, 2025
@jcreedcmu
jcreedcmu force-pushed the jcreed-manual-tex-unit-tests branch from 2bc0dc7 to 35955a7 Compare October 2, 2025 20:56
@jcreedcmu
jcreedcmu merged commit 6bda0f0 into leanprover:main Oct 7, 2025
4 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.

1 participant