Skip to content

Sorry

Viktor Kuncak requested to merge github/fork/SimonGuilloud/sorry into main

Created by: SimonGuilloud

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.

Merge request reports