search

epfl-lara / lisa

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

When constructing a theorem, parse the provided statement and compare it to the proof conclusion #59

Closed cache-nez closed 1 year ago

SimonGuilloud commented 2 years ago

Please leave the check in the RunningTheory as it was, it is not needed for this feature :)

cache-nez commented 2 years ago

@SimonGuilloud dropped.

Fixes #9.

cache-nez commented 2 years ago

Do we have any tests checking that we correctly reject a theorem if the statement given is wrong?

Thanks for reminding, pushed this test now.