diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-23 21:19:47 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-23 21:19:47 +0200 |
| commit | f273a3fd299796a5f2e5b1ec83f2d87621b4ae73 (patch) | |
| tree | e933e67ef5222833ebff33356b63adce863f7f92 /source/Checking.hs | |
| parent | d1d3f178db000a6ffd928a75af8eb1ba2b7f8b9a (diff) | |
Make `Contradiction` a proof-terminal keyword
Diffstat (limited to 'source/Checking.hs')
| -rw-r--r-- | source/Checking.hs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index f80e164..f6402f6 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -1249,6 +1249,10 @@ checkProof = \case gets blockEndLocation setLocation loc justify j + Contradiction loc j -> do + setLocation loc + setGoals [Bottom] + justify j ByContradiction loc proof -> do setLocation loc goals <- gets checkingGoals |