tex generation: \rm-->\mathrm and \usepackage{...}

metamath / metamath-exe

Metamath program - source code for the Metamath executable

GNU General Public License v2.0

77 stars 25 forks source link

tex generation: \rm-->\mathrm and \usepackage{...} #131

Closed benjub closed 1 year ago

benjub commented 1 year ago

This is the non-style part of #130.

digama0 commented 1 year ago

It would be nice if we had a test case for tex generation (not checking that it compiles, but just a straight input-output test) so we can make sure it works. But making the test suite handle tex tests is more work than I think should go in this PR so I'll merge it as is.