search

epfl-lara / lisa

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

Print errors from proof tactics in meaningful way #85

Closed SimonGuilloud closed 1 year ago

SimonGuilloud commented 1 year ago

THe new tactics can show errors, but they for now do so in a non-useful way. We need to be able to print proofs (with the proof tactics, no just SC) and show there the fault.

sankalpgambhir commented 1 year ago

This should be fixed with #99 . Any other additions needed for this, @SimonGuilloud ?

sankalpgambhir commented 1 year ago

Fixed with #99 and #101 .