search

epfl-lara / lisa

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

Better Feedback for Failed Substitutions #170

Closed sankalpgambhir closed 1 year ago

sankalpgambhir commented 1 year ago

Failed substitutions now print the formula which could not be substituted. Minor change, but I find myself looking for what failed often.

Old

[info]               thenHave(fun(t1, y1) /\ fun(t2, y1)) by Substitution.apply2(false, y1 === y2)
[info]    Proof tactic Substitution used in.(Recursion.scala:463) did not succeed:
[info]    Could not rewrite RHS of premise into conclusion with given substitutions.

New

[info]               thenHave(fun(t1, y1) /\ fun(t2, y1)) by Substitution.apply2(false, y1 === y2)
[info]    Proof tactic Substitution used in.(Recursion.scala:463) did not succeed:
[info]    Could not rewrite RHS of premise into conclusion with given substitutions.
[info] Formula: functionalOver('t1, initialSegment('p, 'y1))

Not necessarily intended to be merged immediately. If you have suggestions for how we can make the feedback better, we can add it to this PR as well.