diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-02-22 17:23:42 +0100 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-02-22 17:23:42 +0100 |
| commit | bc281d5b4b3f6f91592ec838334628e8756b97da (patch) | |
| tree | 4a25a0877fb50c1d9051ae51f96019c534c54d53 | |
| parent | 3980f4d120b03d44330938b50be3ee4aeb7d3015 (diff) | |
Add `INVARIANT` note to `checkingGoals`
| -rw-r--r-- | source/Checking.hs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index 4e0281e..98f5463 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -96,7 +96,7 @@ data CheckingState = CheckingState -- ^ Local assumptions (cached encoding). -- , checkingGoals :: [Formula] - -- ^ The current goals. + -- ^ The current goals. INVARIANT: these should always be canonicalized and have all abbreviations resolved. -- , checkingFacts :: InsOrdMap Marker Hypothesis -- ^ Axioms and proven results (cached encoding). |