search

epfl-lara / lisa

Proof assistant based on first-order logic and set theory
Apache License 2.0
33 stars 18 forks source link

Added tests to Substitution functions #82

Closed lighthea closed 1 year ago

lighthea commented 1 year ago

Added tests to test both functionalities of simple formulas/terms of each type and corner cases for every substitution functions. Until issues #74, #80, and #81 are closed 4 tests are commented out

SimonGuilloud commented 1 year ago

you could retry the tests which are not passing now :)

cache-nez commented 1 year ago

Until issues 74, 80, and 81 are closed 4 tests are commented out

You can refer to issues like that: #81, then this reference appears on the issue page (in this case, I'll know I'm blocking your PR!). There is also an alternative to commenting tests out: one can write ignore(name) { body } instead of test(name) { body }, which will produce an output (making it easier to remember about and investigate the disabled test) without failing the CI.

lighthea commented 1 year ago

Thank you for the formatting tips, the tests depending on the isSame problem are running correctly now

SimonGuilloud commented 1 year ago

Hmmm why are some cases removed from UNconditionalizeProof?

sankalpgambhir commented 1 year ago

Substitution tests were written in #106.