search

metamath / metamath-knife

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

Fix parsing issue #32 #33

Closed tirix closed 2 years ago

tirix commented 2 years ago

Unit test shall fail... until I find the fix!

tirix commented 2 years ago

The issue was with the "type conversion" step of the grammar tree, in case two variables follow each other in a syntax construct without any constant in between, like for the operation value ( A O B ), or the binary operator A R B.

In that case, the offset of the reduce had to be increased, because that reduce has to occur on the variable read before the current reduce.