diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-02 12:27:49 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-02 12:27:49 +0200 |
| commit | e827efe3db5d62fab5fc6dc9c3d15b8488af6b09 (patch) | |
| tree | f3bf07d364aaaf2309871a0e8027080fdd9e531b /source/Checking/Core.hs | |
| parent | 70f2b2b2c2b91a74280847cd9d465374953f7c1d (diff) | |
Prepare exact claim envelopes
Diffstat (limited to 'source/Checking/Core.hs')
| -rw-r--r-- | source/Checking/Core.hs | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index e555151..4368fed 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -47,6 +47,8 @@ module Checking.Core , checkScopedCanonicalCore , embedClosedCore , weakenScopedCore + , implyScopedCore + , closeScopedForall , openScopedForall , openScopedImplication , closeScopedCore @@ -679,6 +681,37 @@ weakenScopedCore globalType binderType scoped = (shiftCanonical 1 0 (scopedCoreTerm scoped)) +-- | Combine two checked propositions under the same lexical context. +implyScopedCore + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +implyScopedCore + (ScopedCheckedCore premiseContext TyProp premise) + (ScopedCheckedCore conclusionContext TyProp conclusion) + | premiseContext == conclusionContext = + Just + (ScopedCheckedCore + premiseContext + TyProp + (CImp premise conclusion)) +implyScopedCore _premise _conclusion = + Nothing + +-- | Close the nearest checked binder as one leading universal. +closeScopedForall + :: ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +closeScopedForall + (ScopedCheckedCore (binderType : context) TyProp body) = + Just + (ScopedCheckedCore + context + TyProp + (CForall binderType body)) +closeScopedForall _scoped = + Nothing + -- | Open one checked leading universal without rechecking its body. openScopedForall :: ScopedCheckedCore global |