diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-26 12:42:27 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-26 12:42:27 +0200 |
| commit | 108b963ebe395ec7c75234e5069c31732531fc97 (patch) | |
| tree | 1b867bbb798f3ee4e028d618037d04d0db9a922c /source/Syntax/Internal.hs | |
| parent | 86aae60ce793e0c2a2f3e12e744b8739d329d2bb (diff) | |
Make `Omitted` carry its location
Diffstat (limited to 'source/Syntax/Internal.hs')
| -rw-r--r-- | source/Syntax/Internal.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 5037e14..5c2fb8d 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -517,7 +517,7 @@ data CalcQuantifier deriving (Show, Eq, Ord) data Proof - = Omitted + = Omitted Location -- ^ Ends a proof without further verification. -- This results in a “gap” in the formalization. | Qed {mloc :: Maybe Location, by :: Justification} |