search

Formal-Systems-Laboratory / matching-logic-mm0

Formalisation of Matching Logic in Metamath 0
BSD 3-Clause "New" or "Revised" License
0 stars 1 forks source link

Test using `mm0-c` #9

Closed nishantjr closed 1 year ago

nishantjr commented 1 year ago

This PR first refactors the code base, and then enables mm0-c checking of proofs.