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

New trait to support work variables #89

Open tirix opened 2 years ago

tirix commented 2 years ago

This introduces a trait Resolver meant to handle work variables outside of metamath-knife.

The new trait shall be able to resolve work variable names like e.g. &W1 into a virtual symbol, as well as into the corresponding a virtual floating axiom, and vice-versa for printing back that symbol.

An implementation is provided in the form of Nameset, which does not resolve any additional work variables, but only regular symbols straight from the database.

david-a-wheeler commented 2 years ago

I haven't had time to review the code, but the idea makes complete sense. If no one objects for a while, I'd say merge it. I'd like to hear from @digama0 if he has a chance to review it.