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 10 forks source link

Add a Debug implementation for substitutions. #45

Closed tirix closed 2 years ago

tirix commented 2 years ago

Note: the second commit has nothing to do with the PR title, but is only due to a new clippy lint which appeared recently.

digama0 commented 2 years ago

Regarding the clippy lint, I noticed this one in one of my cleanup PRs earlier and decided not to apply it, although I think it was nightly at the time so I couldn't #[allow] it. The reasoning is that the original code is shorter and is effectively emulating a do-while loop in rust, and also IIRC this example was reported on clippy and it might get less aggressive about this case in the future. (Otherwise LGTM.)

tirix commented 2 years ago

I can revert it : the do-while loop is indeed quite readable. Did you mean to allow that lint just for that function, or the whole lib.rs?

digama0 commented 2 years ago

Either one is fine by me. Turning it off globally is probably fine since the lint is also wrong (it is suggesting moving the condition out of the loop), so it will probably get fixed upstream at some point.