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

Commands #106

Closed tirix closed 1 year ago

tirix commented 1 year ago

A proposal to move $j command interpretation to a lazily evaluated Commands struct, as discussed in #103. Currently only supports the syntax command, but more could be added. Grammar can be later refitted to use this struct.

tirix commented 1 year ago

There was no feedback to this PR, but it looks like we are moving towards an architecture where $j commands are handled separately in each "pass".

As a result, command check results are available in the corresponding pass, (e.g. provable typecode in the Grammar pass, and primitive commands in the definition pass) so there is no need to store them in a central place.

So I will close this PR if there is no objection.