This PR ensures that the body of proofs used by Pi Squared to test the math proof tests will be tested as regression tests for the proof hint emitter and parser. We do this by folding all of these small examples into the existing test suite.
It's a pretty large PR but mostly just adds the definition.kore versions of the k-files files, and the .kore input files taken by parsing the programs found in the pi2 repo. We then commit the verbose proof hint that these examples generate.
There is a pretty simple way to regenerate the output files that I can show anyone who is interested in the future if they need to modify the results when the proof hints change.
This PR ensures that the body of proofs used by Pi Squared to test the math proof tests will be tested as regression tests for the proof hint emitter and parser. We do this by folding all of these small examples into the existing test suite.
It's a pretty large PR but mostly just adds the definition.kore versions of the k-files files, and the .kore input files taken by parsing the programs found in the pi2 repo. We then commit the verbose proof hint that these examples generate.
There is a pretty simple way to regenerate the output files that I can show anyone who is interested in the future if they need to modify the results when the proof hints change.