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

Fix parsing issue #43 #44

Closed tirix closed 2 years ago

tirix commented 2 years ago

Added a unit test which exhibits issue #43

tirix commented 2 years ago

The issue was with the "garden path" step of the grammar build, in case one of the path had a "reduce" step and the other hadn't. That missing reduce had to be caught up when building the path to recover the errances on the garden path.