metamath / metamath-knife

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

Create a battery of input/output tests comparable to SMM2 #10

Open tirix opened 3 years ago

tirix commented 3 years ago

See SMM3's PR#1. Quoting @sorear :

I'd like it to be approximately as thorough as the SMM2 tests, and some of them could probably be reused as is, although the grammar is significantly different and will hit errors in a different order, and something needs to be done to test incremental operation but I'm not sure what that would look like yet.