search

metamath / metamath-knife

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

Statement parse errors in some set.mm versions #121

Open tirix opened 1 year ago

tirix commented 1 year ago

Since set.mm's commit ee877d4, the grammar pass fails with the following error message:

error: Unparseable statement
     --> ../set.mm/set.mm:11907:28
      |
11907 |     trujust $p |- ( ( A. x x = x -> A. x x = x )
      |                            ^ Could not parse this statement
      |
error: Can't build the grammar
      --> ../set.mm/set.mm:456456:3
       |
456456 |     $( $j garden_path ( x   =>   ( ph ;
       |  ___^
...      |
456462 | |   $)
       | |____^ Expanded formula cannot be parsed from root node
       |
2 diagnostics issued.

It should not be the case, and the changes in that commit seem to be completely unrelated.