Add a `convert_to_provable` parameter to `parse_formula`

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

Closed tirix closed 2 years ago

tirix commented 2 years ago

To allow to create directly a formula with provable type code.

This also includes changes to the Formula API which allow to:

accumulate substitutions when performing unfication : this allows to unify several formulas, e.g. when there essential hypotheses,
complete missing substitutions : this allows introducing work variables, e.g. for C in the case of ( A + C ) = ( B + C ) |- A = B,
iterate through a Formula's labels

tirix commented 2 years ago

Thanks for your remarks @digama0 ! If there's nothing else I'd like to merge this PR and move on!