This PR allows having introducing val for tests, which may get created by some phases (e.g. the test in separate/Model contains binding introduced by RefinementLifting).
For unequivalence, it also outputs the expected result as well as the result from the candidate function.
This PR allows having introducing
val
for tests, which may get created by some phases (e.g. the test inseparate/Model
contains binding introduced byRefinementLifting
). For unequivalence, it also outputs the expected result as well as the result from the candidate function.