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

Substitute sub-formulas #93

Closed tirix closed 1 year ago

tirix commented 1 year ago

I recently dug up my rumm proof of concept and found out in some cases I need not just substitution of variables, but also substitution of whole sub-formulas.

This adds this functionality, together with the relevant test.