Extracted a `parse_formula` library API to parse a single formula

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

Extracted a `parse_formula` library API to parse a single formula #22

Closed tirix closed 3 years ago

tirix commented 3 years ago

This makes the grammar module's parse_formula function public, by:

using an iterator over symbols, rather than a reference to a database statement,
removing the private formula_builder from its parameters.

This change allows a user of the library to parse not just existing database statements, but also new statements, without the need to add them to the database.