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

Discouraged file path can be specified on the command line #97

Closed tirix closed 1 year ago

digama0 commented 1 year ago

Since regen_discouraged and output_discouraged are basically the same thing now, I combined them into one function and moved the file handling into the command line tool itself. Also the scope pass is not necessary for discouraged generation, so I made it optional and now it only takes 241ms to generate the discouraged file for set.mm.

tirix commented 1 year ago

Ok for the changes! I just think the dummy closure is maybe a bit hard to read. I wanted to propose a small change but I was just one minute too slow, so I created a new PR, #98