Erroneous parsing - Githubissues

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

Closed tirix closed 2 years ago

tirix commented 2 years ago

I've noticed that formulas in the form |- ( x A B ) = C are not parsed correctly. The correct syntax tree would be:

wceq
- cov
  - cv
    - vx
  - cA
  - cB
- cC

The actual result is:

wceq
- cov
  - vx
  - cv
    - cA
  - cB
- cC

tirix commented 2 years ago

Fixed with #33