david-a-wheeler / mmverify.py

Metamath verifier in Python
MIT License
35 stars 10 forks source link

Faster #8

Closed benjub closed 2 years ago

benjub commented 2 years ago

To @tirix, @david-a-wheeler: I am pushing this small PR now because of a funny bug happening at metamath/set.mm: in https://github.com/metamath/set.mm/blob/develop/.github/workflows/verifiers.yml, a faster version of mmverify.py is created by stripping the lines with 'vprint'. However, this created an indentation problem in the resulting file (see in the code diffs below why).