diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-02 09:39:50 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-02 09:39:50 +0200 |
| commit | bb84c7baa15d11d2d63721b1f975aac94dc0f211 (patch) | |
| tree | 02c1783cb67fc16aab8062261c50198b3b5fe157 /source/Checking/Exact | |
| parent | e3a24b91d137e00a1f7f6a9d2946bc301e9499c9 (diff) | |
Authorize exact guarded rule sets
Diffstat (limited to 'source/Checking/Exact')
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs index 6ab1f8c..707ff15 100644 --- a/source/Checking/Exact/Inductive.hs +++ b/source/Checking/Exact/Inductive.hs @@ -626,8 +626,9 @@ commitPreparedExactInductive where authorizeFact candidate fact = Declaration.authorizeKernelConstructionCandidate - (GuardedFoundationRule - (Typed.typedInductiveFactRule fact)) + (GuardedFoundationRules + (guardedRuleSet + (Typed.typedInductiveFactRules fact))) candidate do traverse_ Declaration.useAuthorizedFact guards pure (Typed.typedInductiveFactDerivation fact) @@ -660,9 +661,9 @@ encodePreparedInductive key alias typed = putCanonicalTermCache putObjectIdCache (frozenCoreTerm (Typed.typedInductiveFactTarget fact)) - putCacheBytes - (encodeKernelRuleTag - (Typed.typedInductiveFactRule fact)) + putCacheList + (putCacheBytes . encodeKernelRuleTag) + (toList (Typed.typedInductiveFactRules fact)) firstDuplicate :: Ord value => [value] -> Maybe value firstDuplicate = |