epfl-lara / lisa

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

Sorry #155

Closed SimonGuilloud closed 1 year ago

SimonGuilloud commented 1 year ago

Add a "Sorry" proof step that can justify any conclusion, but marks theorems using it as untrustworthy.

Proven Theorems (but not Lemmas and Corollaries) get automatically printed. If a theorem is untrustworthy, it is shown in yellow with a warning.