metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 10 forks source link

Additional grammar tests, iterative parsing #21

Closed tirix closed 2 years ago

tirix commented 2 years ago

This adds several new grammar tests:

Also, the parse_formula function was recursive, which required many function arguments. This function is now iterative, and much fewer arguments are required.