Flag for assigning atoms to statement labels

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

Flag for assigning atoms to statement labels #39

Open tirix opened 2 years ago

tirix commented 2 years ago

Currently, the incremental flag (command line repeat option) has two uses:

it enables automatic reload of the database and incremental builds,
it activates assigning atoms to statement labels

Assigning atoms to statement labels is also used by the grammar statement parsing, as statement atoms (Label) are used as nodes in formula syntax trees.

We shall probably decouple the two.