Prepare exact inductive declarations

author: adelon <22380201+adelon@users.noreply.github.com> 2026-08-02 02:33:14 +0200
committer: adelon <22380201+adelon@users.noreply.github.com> 2026-08-02 02:33:14 +0200
commit: d55d2416bc4f6a9aa055a17deae4fba0fe906316 (patch)
tree: 4a248850088bc0aad1b5084062abc385008d6d87 /source
parent: 118fd4a72f01ebfcedd2c75c2f34cc46e9692586 (diff)
9 files changed, 1435 insertions, 263 deletions
diff --git a/source/Checking.hs b/source/Checking.hs
index 14d0381..5c24d4d 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -3253,6 +3253,7 @@ checkTypedInductive context checked builder st = do
             )
             pure
             (TypedInductive.prepareTypedInductive
+                Transition.checkedGlobalType
                 (Transition.transitionBuilderFoundation
                     builder)
                 (typedSourceGlobal builder)
@@ -3349,7 +3350,9 @@ directInductive context checked =
 typedSourceGlobal
     :: Transition.TransitionModuleBuilder
     -> Symbol
-    -> Maybe TypedInductive.SourceGlobal
+    -> Maybe
+        (TypedInductive.SourceGlobal
+            Transition.CheckedGlobalRef)
 typedSourceGlobal builder symbol = do
     reference <-
         Transition.lookupTransitionGlobal
@@ -3400,6 +3403,7 @@ commitTypedInductiveFact
     -> Vector Transition.TransitionDerivationImport
     -> Transition.TransitionModuleBuilder
     -> TypedInductive.PreparedTypedInductiveFact
+        Transition.CheckedGlobalRef
     -> CheckingM Transition.TransitionModuleBuilder
 commitTypedInductiveFact context imports builder fact = do
     either
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs
index ce4f0cf..e555151 100644
--- a/source/Checking/Core.hs
+++ b/source/Checking/Core.hs
@@ -43,6 +43,7 @@ module Checking.Core
     , scopedCoreContext
     , scopedCoreType
     , scopedCoreTerm
+    , mapScopedGlobals
     , checkScopedCanonicalCore
     , embedClosedCore
     , weakenScopedCore
@@ -634,6 +635,17 @@ scopedCoreTerm
         (ScopedCheckedCore _context _coreType term) =
     term
 
+mapScopedGlobals
+    :: (left -> right)
+    -> ScopedCheckedCore left
+    -> ScopedCheckedCore right
+mapScopedGlobals transform
+        (ScopedCheckedCore context coreType term) =
+    ScopedCheckedCore
+        context
+        coreType
+        (mapCanonicalGlobals transform term)
+
 checkScopedCanonicalCore
     :: (global -> Maybe CoreType)
     -> [CoreType]
diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs
index 777d7a6..94aeef8 100644
--- a/source/Checking/Declaration.hs
+++ b/source/Checking/Declaration.hs
@@ -18,6 +18,7 @@ module Checking.Declaration
     , nextDeclarationSlotDriver
     , currentTheoryDriver
     , resolveVisibleFactAliasDriver
+    , resolveVisibleFactTargetsDriver
     , resolveVisibleGlobalDriver
     , resolveVisibleGlobalContentDriver
     , objectAvailableDriver
@@ -41,6 +42,7 @@ module Checking.Declaration
     , reserveCandidateBatch
     , reservePropositionCandidate
     , reserveDefinitionEquationCandidate
+    , reserveDefinitionEquationCandidateBatch
     , reservedCandidateSlot
     , reservedCandidateStage
     , CandidateProof
@@ -854,6 +856,19 @@ resolveVisibleFactAliasDriver alias = ModuleDriver do
             Map.lookup alias (logicalBuilderAliases builder)
         pure fingerprint
 
+resolveVisibleFactTargetsDriver
+    :: FrozenCheckedCore ObjectId
+    -> ModuleDriver failure
+        [SemanticFactOccurrenceFingerprint]
+resolveVisibleFactTargetsDriver target = ModuleDriver do
+    DriverState _resolver builder _prefix _validation <- State.get
+    pure
+        [ fingerprint
+        | (fingerprint, AuthorizedFact proposition _occurrence _authorization) <-
+            Map.toAscList (logicalBuilderFacts builder)
+        , checkedPropositionTerm proposition == target
+        ]
+
 resolveVisibleGlobalDriver
     :: SemanticGlobalKey
     -> ModuleDriver failure (Maybe (SemanticGlobalTarget, CoreType))
@@ -1250,6 +1265,103 @@ reserveDefinitionEquationCandidate identity alias = Declaration do
                 SearchEligible
                 [alias]))
 
+-- | Reserve one defining equation and a nonempty generated-fact batch at the
+-- same declaration stage. No candidate in the batch can cite a sibling.
+reserveDefinitionEquationCandidateBatch
+    :: ObjectId
+    -> SemanticName
+    -> NonEmpty
+        ( ScopedCheckedCore ObjectId
+        , FactSearchEligibility
+        , [SemanticName]
+        )
+    -> Declaration
+        ( ReservedCandidate
+        , NonEmpty ReservedCandidate
+        )
+reserveDefinitionEquationCandidateBatch identity alias generated =
+    Declaration do
+        unprepared <- State.get
+        prepared <-
+            State.lift
+                (Except.liftEither
+                    (prepareDeclarationClosure unprepared))
+        let closure =
+                maybe
+                    (impossible
+                        "prepared declaration closure is absent")
+                    id
+                    (declarationObjectClosure prepared)
+        content <-
+            maybe
+                (State.lift
+                    (Except.throwError
+                        (DefinitionEquationObjectMissing identity)))
+                pure
+                (lookupCheckedObjectContent identity closure)
+        (coreType, body) <-
+            case content of
+                TransparentObjectContent _theory objectType objectBody ->
+                    pure (objectType, objectBody)
+                _ ->
+                    State.lift
+                        (Except.throwError
+                            (DefinitionEquationObjectNotTransparent identity))
+        definition <-
+            State.lift
+                (Except.liftEither
+                    (first DeclarationPropositionValidationFailed
+                        (validatePropositionContent
+                            closure
+                            (CEq
+                                coreType
+                                (CGlobal identity)
+                                body))))
+        generatedSpecs <-
+            traverse
+                (prepareGeneratedSpec closure)
+                generated
+        State.put prepared
+        candidates <-
+            runDeclaration
+                (reserveCandidateBatch
+                    ( candidateSpec
+                        definition
+                        SearchEligible
+                        [alias]
+                    :| toList generatedSpecs
+                    ))
+        case candidates of
+            definitionCandidate :| firstGenerated : remainingGenerated ->
+                pure
+                    ( definitionCandidate
+                    , firstGenerated :| remainingGenerated
+                    )
+            _ ->
+                impossible
+                    "a nonempty generated batch produced no candidate"
+  where
+    prepareGeneratedSpec closure (scoped, eligibility, aliases) = do
+        frozen <-
+            maybe
+                (State.lift
+                    (Except.throwError CandidatePropositionNotClosed))
+                pure
+                (closeScopedCore scoped)
+        unless (frozenCoreType frozen == TyProp)
+            (State.lift
+                (Except.throwError
+                    (CandidatePropositionNotProposition
+                        (frozenCoreType frozen))))
+        proposition <-
+            State.lift
+                (Except.liftEither
+                    (first DeclarationPropositionValidationFailed
+                        (validatePropositionContent
+                            closure
+                            (frozenCoreTerm frozen))))
+        pure (candidateSpec proposition eligibility aliases)
+
 -- | Resolve one complete compiled declaration against its exact validation
 -- key, then run the source-level authorization action under that selection.
 -- Objects and candidates must already be prepared so the lookup key cannot
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs
new file mode 100644
index 0000000..cbb29f0
--- /dev/null
+++ b/source/Checking/Exact/Inductive.hs
@@ -0,0 +1,742 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact preparation and atomic publication of direct set inductives.
+module Checking.Exact.Inductive
+    ( PreparedExactInductive
+    , preparedExactInductiveCarrierId
+    , preparedExactInductiveCarrierType
+    , preparedExactInductiveCarrierBody
+    , preparedExactInductiveGuardTargets
+    , preparedExactInductiveFacts
+    , prepareExactInductive
+    , commitPreparedExactInductive
+    , ExactInductiveError(..)
+    , exactInductiveErrorLocation
+    , renderExactInductiveError
+    ) where
+
+import Base hiding (Empty)
+import Checking.Authority
+import Checking.Core
+import Checking.Declaration qualified as Declaration
+import Checking.Foundation
+import Checking.Identity
+import Checking.Semantic
+import Checking.Typed.Inductive qualified as Typed
+import Felix.Cache.Codec
+import Meaning qualified
+import Report.Location
+import Syntax.Abstract qualified as Raw
+import Syntax.Interface
+import Syntax.Internal qualified as Internal
+import Syntax.Lexicon
+    ( pattern ConsSymbol
+    , pattern PairSymbol
+    )
+
+import Control.Monad (foldM, unless, when)
+import Control.Monad.Except (ExceptT)
+import Control.Monad.Except qualified as Except
+import Data.Bifunctor (first)
+import Data.ByteString (ByteString)
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Maybe (catMaybes)
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import Data.Vector qualified as Vector
+
+
+data PreparedExactInductive = PreparedExactInductive
+    !Location
+    !SemanticGlobalKey
+    !ObjectId
+    !(Maybe AssertedObject)
+    !SemanticName
+    !DeclarationSyntaxId
+    !(Typed.PreparedTypedInductive ObjectId)
+    ![SemanticFactOccurrenceFingerprint]
+
+preparedExactInductiveCarrierId
+    :: PreparedExactInductive
+    -> ObjectId
+preparedExactInductiveCarrierId
+        (PreparedExactInductive
+            _location _key identity _asserted _alias _syntax _typed _guards) =
+    identity
+
+preparedExactInductiveCarrierType
+    :: PreparedExactInductive
+    -> CoreType
+preparedExactInductiveCarrierType
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveCarrierType typed
+
+preparedExactInductiveCarrierBody
+    :: PreparedExactInductive
+    -> FrozenCheckedCore ObjectId
+preparedExactInductiveCarrierBody
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveCarrierBody typed
+
+preparedExactInductiveGuardTargets
+    :: PreparedExactInductive
+    -> Vector.Vector (FrozenCheckedCore ObjectId)
+preparedExactInductiveGuardTargets
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveGuardTargets typed
+
+preparedExactInductiveFacts
+    :: PreparedExactInductive
+    -> NonEmpty (Typed.PreparedTypedInductiveFact ObjectId)
+preparedExactInductiveFacts
+        (PreparedExactInductive
+            _location _key _identity _asserted _alias _syntax typed _guards) =
+    Typed.typedInductiveFacts typed
+
+data ExactInductiveError
+    = ExactInductiveUnsupportedBlock !Location
+    | ExactInductiveOccurrenceMissing !Location
+    | ExactInductiveOccurrenceAmbiguous !Location
+    | ExactInductiveHeadMismatch !Location
+    | ExactInductiveGlossFailed !Location !Meaning.GlossError
+    | ExactInductiveDuplicateParameter !Location !Internal.VarSymbol
+    | ExactInductiveDomainFreeVariable !Location !Internal.VarSymbol
+    | ExactInductiveDomainMentionsCarrier !Location
+    | ExactInductiveResultShape !Location
+    | ExactInductiveResultMentionsCarrier !Location
+    | ExactInductiveRecursiveTermMentionsCarrier !Location
+    | ExactInductiveNestedRecursion !Location
+    | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey
+    | ExactInductiveGlobalNotVisible !Location !Internal.Symbol
+    | ExactInductiveGlobalAmbiguous !Location !Internal.Symbol
+    | ExactInductiveGlobalContentInvalid !Location !CoreCheckError
+    | ExactInductivePreparationFailed
+        !Location
+        !Typed.TypedInductiveError
+    | ExactInductiveGuardMissing !Location
+    | ExactInductiveGuardAmbiguous !Location
+    deriving stock (Show, Eq)
+
+exactInductiveErrorLocation :: ExactInductiveError -> Location
+exactInductiveErrorLocation = \case
+    ExactInductiveUnsupportedBlock location -> location
+    ExactInductiveOccurrenceMissing location -> location
+    ExactInductiveOccurrenceAmbiguous location -> location
+    ExactInductiveHeadMismatch location -> location
+    ExactInductiveGlossFailed location _failure -> location
+    ExactInductiveDuplicateParameter location _parameter -> location
+    ExactInductiveDomainFreeVariable location _variable -> location
+    ExactInductiveDomainMentionsCarrier location -> location
+    ExactInductiveResultShape location -> location
+    ExactInductiveResultMentionsCarrier location -> location
+    ExactInductiveRecursiveTermMentionsCarrier location -> location
+    ExactInductiveNestedRecursion location -> location
+    ExactInductiveGlobalAlreadyVisible location _key -> location
+    ExactInductiveGlobalNotVisible location _symbol -> location
+    ExactInductiveGlobalAmbiguous location _symbol -> location
+    ExactInductiveGlobalContentInvalid location _failure -> location
+    ExactInductivePreparationFailed location _failure -> location
+    ExactInductiveGuardMissing location -> location
+    ExactInductiveGuardAmbiguous location -> location
+
+renderExactInductiveError :: ExactInductiveError -> Text
+renderExactInductiveError failure =
+    locationToText (exactInductiveErrorLocation failure)
+        <> ": "
+        <> case failure of
+            ExactInductiveUnsupportedBlock{} ->
+                "this inductive source form is not supported by the typed checker"
+            ExactInductiveOccurrenceMissing{} ->
+                "the inductive declaration has no associated syntax occurrence"
+            ExactInductiveOccurrenceAmbiguous{} ->
+                "the inductive declaration has more than one semantic head"
+            ExactInductiveHeadMismatch{} ->
+                "the inductive head does not match its syntax occurrence"
+            ExactInductiveGlossFailed _location glossFailure ->
+                "inductive elaboration failed: " <> shown glossFailure
+            ExactInductiveDuplicateParameter _location parameter ->
+                "the inductive parameter is repeated: " <> shown parameter
+            ExactInductiveDomainFreeVariable _location variable ->
+                "the inductive domain contains an unbound variable: "
+                    <> shown variable
+            ExactInductiveDomainMentionsCarrier{} ->
+                "the inductive domain must be independent of its carrier"
+            ExactInductiveResultShape{} ->
+                "an inductive result must have the form t \\in F(args)"
+            ExactInductiveResultMentionsCarrier{} ->
+                "an inductive result term must not mention its carrier"
+            ExactInductiveRecursiveTermMentionsCarrier{} ->
+                "a recursive occurrence must be in the carrier of a membership premise"
+            ExactInductiveNestedRecursion{} ->
+                "nested inductive recursion is not supported by the typed checker"
+            ExactInductiveGlobalAlreadyVisible _location key ->
+                "the inductive carrier is already visible: " <> shown key
+            ExactInductiveGlobalNotVisible _location symbol ->
+                "an inductive source symbol is not visible: " <> shown symbol
+            ExactInductiveGlobalAmbiguous _location symbol ->
+                "an inductive source symbol has more than one meaning: "
+                    <> shown symbol
+            ExactInductiveGlobalContentInvalid _location coreFailure ->
+                "an inductive global has invalid checked content: "
+                    <> shown coreFailure
+            ExactInductivePreparationFailed _location typedFailure ->
+                "typed inductive preparation failed: " <> shown typedFailure
+            ExactInductiveGuardMissing{} ->
+                "an inductive domain guard has no visible authorized fact"
+            ExactInductiveGuardAmbiguous{} ->
+                "an inductive domain guard matches more than one visible fact"
+  where
+    shown :: Show value => value -> Text
+    shown = Text.pack . show
+
+type Prepare failure =
+    ExceptT
+        ExactInductiveError
+        (Declaration.ModuleDriver failure)
+
+prepareExactInductive
+    :: CheckedFoundation
+    -> Raw.Block
+    -> [CanonicalLexicalEntry]
+    -> Declaration.ModuleDriver failure
+        (Either ExactInductiveError PreparedExactInductive)
+prepareExactInductive foundation block entries =
+    Except.runExceptT do
+        (location, marker, rawInductive) <-
+            case block of
+                Raw.BlockInductive blockLocation _title blockMarker inductive ->
+                    pure (blockLocation, blockMarker, inductive)
+                _ ->
+                    Except.throwError
+                        (ExactInductiveUnsupportedBlock (locate block))
+        key <- validateOccurrence location rawInductive entries
+        visible <-
+            Except.lift
+                (Declaration.resolveVisibleGlobalDriver key)
+        when (isJust visible)
+            (Except.throwError
+                (ExactInductiveGlobalAlreadyVisible location key))
+        internal <-
+            case Meaning.meaning [block] of
+                Right
+                    [Internal.BlockInductive
+                        _internalLocation _internalMarker inductive] ->
+                            pure inductive
+                Left failure ->
+                    Except.throwError
+                        (ExactInductiveGlossFailed location failure)
+                Right _ ->
+                    Except.throwError
+                        (ExactInductiveUnsupportedBlock location)
+        direct <-
+            Except.liftEither
+                (normalizeDirectInductive internal)
+        (sourceGlobals, globalTypes) <-
+            resolveSourceGlobals location internal direct
+        typed <-
+            Except.liftEither
+                (first
+                    (ExactInductivePreparationFailed location)
+                    (Typed.prepareTypedInductive
+                        (requireGlobalType globalTypes)
+                        foundation
+                        (`Map.lookup` sourceGlobals)
+                        marker
+                        direct))
+        guards <-
+            traverse
+                (resolveGuard location)
+                (Vector.toList
+                    (Typed.typedInductiveGuardTargets typed))
+        theory <- Except.lift Declaration.currentTheoryDriver
+        let carrierType = Typed.typedInductiveCarrierType typed
+            carrierBody = Typed.typedInductiveCarrierBody typed
+            carrierTerm = frozenCoreTerm carrierBody
+            identity =
+                transparentObjectId theory carrierType carrierTerm
+            content =
+                TransparentObjectContent theory carrierType carrierTerm
+            alias = case marker of
+                Raw.Marker name -> semanticName name
+        available <-
+            Except.lift
+                (Declaration.objectAvailableDriver identity)
+        let asserted
+                | available = Nothing
+                | otherwise = Just (assertedObject identity content)
+            syntax =
+                declarationSyntaxId
+                    (encodePreparedInductive key alias typed)
+        pure
+            (PreparedExactInductive
+                location
+                key
+                identity
+                asserted
+                alias
+                syntax
+                typed
+                guards)
+  where
+    requireGlobalType types identity =
+        fromMaybe
+            (impossible
+                "prepared inductive global has no checked type")
+            (Map.lookup identity types)
+
+validateOccurrence
+    :: Location
+    -> Raw.Inductive
+    -> [CanonicalLexicalEntry]
+    -> Prepare failure SemanticGlobalKey
+validateOccurrence location rawInductive entries = do
+    entry <-
+        case entries of
+            [] ->
+                Except.throwError
+                    (ExactInductiveOccurrenceMissing location)
+            [single] -> pure single
+            _ ->
+                Except.throwError
+                    (ExactInductiveOccurrenceAmbiguous location)
+    key <-
+        maybe
+            (Except.throwError
+                (ExactInductiveHeadMismatch location))
+            pure
+            (semanticGlobalKeyFromLexicalEntry entry)
+    let Raw.SymbolPattern headSymbol _parameters =
+            Raw.inductiveSymbolPattern rawInductive
+        expected =
+            SemanticExpressionFunction
+                (Raw.mixfixPattern headSymbol)
+    unless (key == expected)
+        (Except.throwError
+            (ExactInductiveHeadMismatch location))
+    pure key
+
+normalizeDirectInductive
+    :: Internal.Inductive
+    -> Either ExactInductiveError Typed.DirectInductive
+normalizeDirectInductive inductive = do
+    case firstDuplicate (Internal.inductiveParams inductive) of
+        Just duplicate ->
+            Left
+                (ExactInductiveDuplicateParameter
+                    (locate duplicate)
+                    duplicate)
+        Nothing -> pure ()
+    let parameters = Internal.inductiveParams inductive
+        parameterSet = Set.fromList parameters
+        domain = Internal.inductiveDomain inductive
+        carrier = Internal.inductiveSymbol inductive
+        domainVariables =
+            orderedUnique
+                (toList domain)
+    case find (`Set.notMember` parameterSet) domainVariables of
+        Just variable ->
+            Left
+                (ExactInductiveDomainFreeVariable
+                    (locate variable)
+                    variable)
+        Nothing -> pure ()
+    when
+        (Internal.SymbolMixfix carrier
+            `Set.member` Internal.mentionedSymbols domain)
+        (Left
+            (ExactInductiveDomainMentionsCarrier
+                (termLocation domain)))
+    clauses <-
+        traverse
+            (normalizeClause carrier parameters)
+            (Internal.inductiveIntros inductive)
+    pure
+        (Typed.DirectInductive
+            parameters
+            domain
+            clauses)
+
+normalizeClause
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.IntroRule
+    -> Either ExactInductiveError Typed.DirectInductiveClause
+normalizeClause carrier parameters rule = do
+    conditions <-
+        traverse
+            (normalizeCondition carrier parameters)
+            (Internal.introConditions rule)
+    result <-
+        normalizeResult
+            carrier
+            parameters
+            (Internal.introResult rule)
+    let parameterSet = Set.fromList parameters
+        variables =
+            List.filter (`Set.notMember` parameterSet)
+                (orderedUnique
+                    ( concatMap toList
+                        (Internal.introConditions rule)
+                      <> toList result
+                    ))
+    pure
+        (Typed.DirectInductiveClause
+            variables
+            conditions
+            result)
+
+normalizeResult
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.Formula
+    -> Either ExactInductiveError Internal.Term
+normalizeResult carrier parameters = \case
+    Internal.IsElementOf _location result target
+        | not (matchesCarrier carrier parameters target) ->
+            Left (ExactInductiveResultShape (termLocation target))
+        | Internal.SymbolMixfix carrier
+                `Set.member` Internal.mentionedSymbols result ->
+            Left
+                (ExactInductiveResultMentionsCarrier
+                    (termLocation result))
+        | otherwise ->
+            Right result
+    formula ->
+        Left (ExactInductiveResultShape (termLocation formula))
+
+normalizeCondition
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.Formula
+    -> Either ExactInductiveError Typed.DirectInductiveCondition
+normalizeCondition carrier parameters formula
+    | not
+        (Internal.SymbolMixfix carrier
+            `Set.member` Internal.mentionedSymbols formula) =
+        Right (Typed.DirectSideCondition formula)
+    | otherwise =
+        case formula of
+            Internal.IsElementOf _location recursiveTerm recursiveCarrier
+                | Internal.SymbolMixfix carrier
+                        `Set.member`
+                            Internal.mentionedSymbols recursiveTerm ->
+                    Left
+                        (ExactInductiveRecursiveTermMentionsCarrier
+                            (termLocation recursiveTerm))
+                | matchesCarrier carrier parameters recursiveCarrier ->
+                    Right
+                        (Typed.DirectRecursiveCondition recursiveTerm)
+                | otherwise ->
+                    Left
+                        (ExactInductiveNestedRecursion
+                            (termLocation recursiveCarrier))
+            _ ->
+                Left
+                    (ExactInductiveNestedRecursion
+                        (termLocation formula))
+
+matchesCarrier
+    :: Internal.FunctionSymbol
+    -> [Internal.VarSymbol]
+    -> Internal.Term
+    -> Bool
+matchesCarrier carrier parameters = \case
+    Internal.TermSymbol _location (Internal.SymbolMixfix actual) arguments ->
+        actual == carrier
+            && length arguments == length parameters
+            && and
+                (zipWith
+                    (\argument parameter ->
+                        argument == Internal.TermVar parameter)
+                    arguments
+                    parameters)
+    _ -> False
+
+resolveSourceGlobals
+    :: Location
+    -> Internal.Inductive
+    -> Typed.DirectInductive
+    -> Prepare failure
+        ( Map.Map
+            Internal.Symbol
+            (Typed.SourceGlobal ObjectId)
+        , Map.Map ObjectId CoreType
+        )
+resolveSourceGlobals location internal direct =
+    foldM resolve (Map.empty, Map.empty) symbols
+  where
+    carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal)
+    symbols =
+        Set.toAscList
+            ( Set.delete carrier
+                (directSymbols direct)
+                `Set.difference` fixedInductiveSymbols
+            )
+
+    resolve (resolved, types) symbol = do
+        let keys = semanticKeys symbol
+        when (null keys)
+            (Except.throwError
+                (ExactInductiveGlobalNotVisible location symbol))
+        matches <-
+            catMaybes
+                <$> traverse
+                    (Except.lift
+                        . Declaration.resolveVisibleGlobalContentDriver)
+                    keys
+        case matches of
+            [] ->
+                Except.throwError
+                    (ExactInductiveGlobalNotVisible location symbol)
+            [match] -> do
+                (source, sourceTypes) <-
+                    Except.liftEither
+                        (prepareSourceGlobal location match)
+                pure
+                    ( Map.insert symbol source resolved
+                    , Map.union sourceTypes types
+                    )
+            _ ->
+                Except.throwError
+                    (ExactInductiveGlobalAmbiguous location symbol)
+
+prepareSourceGlobal
+    :: Location
+    -> ( SemanticGlobalTarget
+       , ObjectContent
+       , Map.Map ObjectId CoreType
+       )
+    -> Either
+        ExactInductiveError
+        (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
+prepareSourceGlobal location (target, content, dependencies) = do
+    body <-
+        case target of
+            GlobalReference _identity ->
+                Right Nothing
+            TransparentExpansion _identity ->
+                case content of
+                    TransparentObjectContent _theory _coreType canonical ->
+                        Just
+                            <$> first
+                                (ExactInductiveGlobalContentInvalid location)
+                                (checkCanonicalCore
+                                    (`Map.lookup` dependencies)
+                                    canonical)
+                    _ ->
+                        impossible
+                            "validated transparent expansion has opaque content"
+    let identity = semanticGlobalTargetObject target
+        types =
+            Map.insert
+                identity
+                (objectContentType content)
+                dependencies
+    pure (Typed.SourceGlobal identity body, types)
+
+resolveGuard
+    :: Location
+    -> FrozenCheckedCore ObjectId
+    -> Prepare failure SemanticFactOccurrenceFingerprint
+resolveGuard location target = do
+    matches <-
+        Except.lift
+            (Declaration.resolveVisibleFactTargetsDriver target)
+    case matches of
+        [] ->
+            Except.throwError (ExactInductiveGuardMissing location)
+        [fingerprint] ->
+            pure fingerprint
+        _ ->
+            Except.throwError (ExactInductiveGuardAmbiguous location)
+
+directSymbols :: Typed.DirectInductive -> Set.Set Internal.Symbol
+directSymbols direct =
+    Internal.mentionedSymbols (Typed.directInductiveDomain direct)
+        <> foldMap clauseSymbols
+            (Typed.directInductiveClauses direct)
+  where
+    clauseSymbols clause =
+        foldMap conditionSymbols
+                (Typed.directClauseConditions clause)
+            <> Internal.mentionedSymbols
+                (Typed.directClauseResult clause)
+    conditionSymbols = \case
+        Typed.DirectSideCondition formula ->
+            Internal.mentionedSymbols formula
+        Typed.DirectRecursiveCondition term ->
+            Internal.mentionedSymbols term
+
+fixedInductiveSymbols :: Set.Set Internal.Symbol
+fixedInductiveSymbols =
+    Set.fromList
+        [ Internal.SymbolMixfix ConsSymbol
+        , Internal.SymbolMixfix PairSymbol
+        , Internal.SymbolMixfix (unarySymbol "pow")
+        , Internal.SymbolMixfix (unarySymbol "cumul")
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.ElementSymbol)
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.EqSymbol)
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.NeqSymbol)
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.SubseteqSymbol)
+        ]
+  where
+    unarySymbol command =
+        Raw.MixfixItem
+            (Raw.TokenCons (Raw.Command command)
+                (Raw.TokenCons Raw.InvisibleBraceL
+                    (Raw.HoleCons
+                        (Raw.TokenCons Raw.InvisibleBraceR Raw.End))))
+            (Raw.Marker command)
+            Raw.NonAssoc
+
+semanticKeys :: Internal.Symbol -> [SemanticGlobalKey]
+semanticKeys = \case
+    Internal.SymbolMixfix symbol ->
+        [SemanticExpressionFunction (Raw.mixfixPattern symbol)]
+    Internal.SymbolFun item ->
+        let patterns = Raw.lexicalItemSgPlPattern item
+        in [SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)]
+    Internal.SymbolPredicate predicate ->
+        case predicate of
+            Internal.PredicateAdj item ->
+                [ SemanticLeftAdjective (Raw.lexicalItemPattern item)
+                , SemanticRightAdjective (Raw.lexicalItemPattern item)
+                ]
+            Internal.PredicateVerb item ->
+                let patterns = Raw.lexicalItemSgPlPattern item
+                in [SemanticVerb (Raw.sg patterns) (Raw.pl patterns)]
+            Internal.PredicateNoun item ->
+                let patterns = Raw.lexicalItemSgPlPattern item
+                in [SemanticNoun (Raw.sg patterns) (Raw.pl patterns)]
+            Internal.PredicateRelation relation ->
+                [ SemanticRelation
+                    (Raw.relationSymbolToken relation)
+                    (Raw.relationSymbolParameterArity relation)
+                ]
+            Internal.PredicateSymbol{} -> []
+            Internal.PredicateNounStruct{} -> []
+    Internal.SymbolInteger{} -> []
+
+commitPreparedExactInductive
+    :: PreparedExactInductive
+    -> Declaration.ModuleDriver failure
+        ((), Declaration.CommittedDeclarationBatch)
+commitPreparedExactInductive
+        (PreparedExactInductive
+            _location key identity asserted alias syntax typed guards) =
+    Declaration.commitCompiledDeclaration syntax do
+        traverse_ Declaration.addDeclarationObject asserted
+        Declaration.stageSemanticGlobalBinding
+            key
+            (GlobalReference identity)
+        let facts = Typed.typedInductiveFacts typed
+            candidateInputs =
+                fmap
+                    (\fact ->
+                        ( embedClosedCore []
+                            (Typed.typedInductiveFactTarget fact)
+                        , SearchEligible
+                        , [markerAlias
+                            (Typed.typedInductiveFactMarker fact)]
+                        ))
+                    facts
+        (definitionCandidate, factCandidates) <-
+            Declaration.reserveDefinitionEquationCandidateBatch
+                identity
+                alias
+                candidateInputs
+        Declaration.authorizeCompiledDeclaration do
+            Declaration.authorizeDefinitionEquationCandidate
+                identity
+                definitionCandidate
+            sequence_
+                (NonEmpty.zipWith
+                    authorizeFact
+                    factCandidates
+                    facts)
+  where
+    authorizeFact candidate fact =
+        Declaration.authorizeKernelConstructionCandidate
+            (GuardedFoundationRule
+                (Typed.typedInductiveFactRule fact))
+            candidate do
+                traverse_ Declaration.useAuthorizedFact guards
+                pure (Typed.typedInductiveFactDerivation fact)
+
+    markerAlias (Raw.Marker name) =
+        semanticName name
+
+encodePreparedInductive
+    :: SemanticGlobalKey
+    -> SemanticName
+    -> Typed.PreparedTypedInductive ObjectId
+    -> ByteString
+encodePreparedInductive key alias typed =
+    encodeCache do
+        putCacheTag 0x04
+        putSemanticGlobalKeyCache key
+        putCoreTypeCache
+            (Typed.typedInductiveCarrierType typed)
+        putCanonicalTermCache putObjectIdCache
+            (frozenCoreTerm
+                (Typed.typedInductiveCarrierBody typed))
+        putCacheText (semanticNameText alias)
+        putCacheList putFact
+            (toList (Typed.typedInductiveFacts typed))
+  where
+    putFact fact = do
+        let Raw.Marker marker =
+                Typed.typedInductiveFactMarker fact
+        putCacheText marker
+        putCanonicalTermCache putObjectIdCache
+            (frozenCoreTerm
+                (Typed.typedInductiveFactTarget fact))
+        putCacheBytes
+            (encodeKernelRuleTag
+                (Typed.typedInductiveFactRule fact))
+
+firstDuplicate :: Ord value => [value] -> Maybe value
+firstDuplicate =
+    go Set.empty
+  where
+    go _seen [] = Nothing
+    go seen (value : remaining)
+        | value `Set.member` seen = Just value
+        | otherwise =
+            go (Set.insert value seen) remaining
+
+orderedUnique :: Ord value => [value] -> [value]
+orderedUnique =
+    reverse . snd . foldl' step (Set.empty, [])
+  where
+    step (seen, values) value
+        | value `Set.member` seen = (seen, values)
+        | otherwise =
+            (Set.insert value seen, value : values)
+
+termLocation :: Internal.Expr -> Location
+termLocation = \case
+    Internal.TermVar variable -> locate variable
+    Internal.TermSymbol location _symbol _arguments -> location
+    Internal.TermSymbolStruct _symbol expression ->
+        maybe Nowhere termLocation expression
+    Internal.Apply function _arguments -> termLocation function
+    Internal.TermSep variable _bound _predicate -> locate variable
+    Internal.ReplacePred value _domain _bound _predicate -> locate value
+    Internal.ReplaceFun ((variable, _domain) :| _remaining) _value _condition ->
+        locate variable
+    Internal.Connected _connective left _right -> termLocation left
+    Internal.Lambda{} -> Nowhere
+    Internal.Quantified{} -> Nowhere
+    Internal.PropositionalConstant{} -> Nowhere
+    Internal.Not location _term -> location
diff --git a/source/Checking/Identity.hs b/source/Checking/Identity.hs
index 01b2241..fe846dc 100644
--- a/source/Checking/Identity.hs
+++ b/source/Checking/Identity.hs
@@ -9,6 +9,7 @@ module Checking.Identity
     , theoryIdDigest
     , encodeFoundationManifest
     , foundationManifestTags
+    , encodeKernelRuleTag
     , ObjectFamily(..)
     , ObjectId
     , objectId
diff --git a/source/Checking/Kernel/Derivation.hs b/source/Checking/Kernel/Derivation.hs
index 8df5562..65bcc25 100644
--- a/source/Checking/Kernel/Derivation.hs
+++ b/source/Checking/Kernel/Derivation.hs
@@ -12,6 +12,7 @@ module Checking.Kernel.Derivation
     , derivationImportJudgment
     , derivationImportStatement
     , KernelDerivation
+    , mapKernelDerivationGlobals
     , importedFactDerivation
     , localHypothesisDerivation
     , foundationFactDerivation
@@ -167,6 +168,65 @@ data KernelDerivation global
         !(KernelDerivation global)
     deriving stock (Eq)
 
+mapKernelDerivationGlobals
+    :: (left -> right)
+    -> KernelDerivation left
+    -> KernelDerivation right
+mapKernelDerivationGlobals transform = go
+  where
+    scoped = mapScopedGlobals transform
+    go = \case
+        UseImportedFact index ->
+            UseImportedFact index
+        UseLocalHypothesis index ->
+            UseLocalHypothesis index
+        UseFoundationFact tag ->
+            UseFoundationFact tag
+        ImplicationElimination premise implication ->
+            ImplicationElimination (go premise) (go implication)
+        ForallElimination proof argument ->
+            ForallElimination (go proof) (scoped argument)
+        FalsumElimination proof target ->
+            FalsumElimination (go proof) (scoped target)
+        ImplicationIntroduction premise proof ->
+            ImplicationIntroduction (scoped premise) (go proof)
+        ForallIntroduction binderType proof ->
+            ForallIntroduction binderType (go proof)
+        ConvertJudgment proof target plan ->
+            ConvertJudgment (go proof) (scoped target) plan
+        EqualityReflexivity term ->
+            EqualityReflexivity (scoped term)
+        EqualityCongruenceApplication function argument ->
+            EqualityCongruenceApplication (go function) (go argument)
+        EqualityCongruenceLambda binderType proof ->
+            EqualityCongruenceLambda binderType (go proof)
+        EqualityModusPonens equality proof ->
+            EqualityModusPonens (go equality) (go proof)
+        ApplySetLfpBound domain operator ->
+            ApplySetLfpBound (scoped domain) (scoped operator)
+        ApplySetLfpLeast domain operator candidate bounded closed ->
+            ApplySetLfpLeast
+                (scoped domain)
+                (scoped operator)
+                (scoped candidate)
+                (go bounded)
+                (go closed)
+        ApplySetLfpFixed domain operator monotone ->
+            ApplySetLfpFixed
+                (scoped domain)
+                (scoped operator)
+                (go monotone)
+        ApplySetLfpInduct domain operator predicate element
+                monotone member closed ->
+            ApplySetLfpInduct
+                (scoped domain)
+                (scoped operator)
+                (scoped predicate)
+                (scoped element)
+                (go monotone)
+                (go member)
+                (go closed)
+
 importedFactDerivation
     :: ImportIx
     -> KernelDerivation global
diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs
index bdd8803..f6d78ba 100644
--- a/source/Checking/Typed/Inductive.hs
+++ b/source/Checking/Typed/Inductive.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GADTs #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
 -- | Direct checked lowering of the current one-carrier set-valued inductive
@@ -16,6 +17,7 @@ module Checking.Typed.Inductive
     , typedInductiveFacts
     , typedInductiveFactMarker
     , typedInductiveFactTarget
+    , typedInductiveFactRule
     , typedInductiveFactDerivation
     , prepareTypedInductive
     , TypedInductiveError(..)
@@ -26,7 +28,6 @@ import Checking.Core
 import Checking.Foundation
 import Checking.Kernel.Derivation
 import Checking.Kernel.Proof
-import Checking.Transition
 import Syntax.Internal
 import Syntax.Lexicon
     ( pattern PairSymbol
@@ -61,20 +62,44 @@ data DirectInductiveCondition
     = DirectSideCondition !Formula
     | DirectRecursiveCondition !Term
 
-data PreparedTypedInductive = PreparedTypedInductive
+data SourceGlobal global = SourceGlobal
+    !global
+    !(Maybe (FrozenCheckedCore global))
+
+data InductiveGlobal global where
+    InductiveGlobal
+        :: Eq global
+        => !global
+        -> !CoreType
+        -> InductiveGlobal global
+
+instance Eq (InductiveGlobal global) where
+    InductiveGlobal left _leftType
+        == InductiveGlobal right _rightType =
+            left == right
+
+inductiveGlobalIdentity :: InductiveGlobal global -> global
+inductiveGlobalIdentity (InductiveGlobal identity _coreType) =
+    identity
+
+inductiveGlobalType :: InductiveGlobal global -> CoreType
+inductiveGlobalType (InductiveGlobal _identity coreType) =
+    coreType
+
+data PreparedTypedInductive global = PreparedTypedInductive
     !CoreType
-    !(FrozenCheckedCore CheckedGlobalRef)
-    !(Vector (FrozenCheckedCore CheckedGlobalRef))
-    !(NonEmpty PreparedTypedInductiveFact)
+    !(FrozenCheckedCore global)
+    !(Vector (FrozenCheckedCore global))
+    !(NonEmpty (PreparedTypedInductiveFact global))
 
-data PreparedInductiveGuard
+data PreparedInductiveGuard global
     = PreparedFoundationGuard !FoundationAxiomTag
     | PreparedImportedGuard
         !ImportIx
-        !(FrozenCheckedCore CheckedGlobalRef)
+        !(FrozenCheckedCore global)
 
 typedInductiveCarrierType
-    :: PreparedTypedInductive
+    :: PreparedTypedInductive global
     -> CoreType
 typedInductiveCarrierType
         (PreparedTypedInductive
@@ -85,8 +110,8 @@ typedInductiveCarrierType
     carrierType
 
 typedInductiveCarrierBody
-    :: PreparedTypedInductive
-    -> FrozenCheckedCore CheckedGlobalRef
+    :: PreparedTypedInductive global
+    -> FrozenCheckedCore global
 typedInductiveCarrierBody
         (PreparedTypedInductive
             _carrierType
@@ -96,8 +121,8 @@ typedInductiveCarrierBody
     body
 
 typedInductiveGuardTargets
-    :: PreparedTypedInductive
-    -> Vector (FrozenCheckedCore CheckedGlobalRef)
+    :: PreparedTypedInductive global
+    -> Vector (FrozenCheckedCore global)
 typedInductiveGuardTargets
         (PreparedTypedInductive
             _carrierType
@@ -106,16 +131,17 @@ typedInductiveGuardTargets
             _facts) =
     guards
 
-newtype PreparedTypedInductiveFact =
+newtype PreparedTypedInductiveFact global =
     PreparedTypedInductiveFact
         ( Marker
-        , FrozenCheckedCore CheckedGlobalRef
-        , KernelDerivation CheckedGlobalRef
+        , FrozenCheckedCore global
+        , KernelRuleTag
+        , KernelDerivation global
         )
 
 typedInductiveFacts
-    :: PreparedTypedInductive
-    -> NonEmpty PreparedTypedInductiveFact
+    :: PreparedTypedInductive global
+    -> NonEmpty (PreparedTypedInductiveFact global)
 typedInductiveFacts
         (PreparedTypedInductive
             _carrierType
@@ -125,27 +151,35 @@ typedInductiveFacts
     facts
 
 typedInductiveFactMarker
-    :: PreparedTypedInductiveFact
+    :: PreparedTypedInductiveFact global
     -> Marker
 typedInductiveFactMarker
         (PreparedTypedInductiveFact
-            (marker, _target, _derivation)) =
+            (marker, _target, _rule, _derivation)) =
     marker
 
 typedInductiveFactTarget
-    :: PreparedTypedInductiveFact
-    -> FrozenCheckedCore CheckedGlobalRef
+    :: PreparedTypedInductiveFact global
+    -> FrozenCheckedCore global
 typedInductiveFactTarget
         (PreparedTypedInductiveFact
-            (_marker, target, _derivation)) =
+            (_marker, target, _rule, _derivation)) =
     target
 
+typedInductiveFactRule
+    :: PreparedTypedInductiveFact global
+    -> KernelRuleTag
+typedInductiveFactRule
+        (PreparedTypedInductiveFact
+            (_marker, _target, rule, _derivation)) =
+    rule
+
 typedInductiveFactDerivation
-    :: PreparedTypedInductiveFact
-    -> KernelDerivation CheckedGlobalRef
+    :: PreparedTypedInductiveFact global
+    -> KernelDerivation global
 typedInductiveFactDerivation
         (PreparedTypedInductiveFact
-            (_marker, _target, derivation)) =
+            (_marker, _target, _rule, derivation)) =
     derivation
 
 data TypedInductiveError
@@ -193,7 +227,7 @@ lookupEnvironment
     -> InductiveEnvironment
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 lookupEnvironment variable
         (InductiveEnvironment variables) =
     maybe
@@ -204,14 +238,40 @@ lookupEnvironment variable
         (Map.lookup variable variables)
 
 prepareTypedInductive
-    :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    :: Eq global
+    => (global -> CoreType)
+    -> CheckedFoundation
+    -> (Symbol -> Maybe (SourceGlobal global))
     -> Marker
     -> DirectInductive
     -> Either
         TypedInductiveError
-        PreparedTypedInductive
+        (PreparedTypedInductive global)
 prepareTypedInductive
+        globalType
+        foundation
+        resolveGlobal
+        marker
+        inductive =
+    mapPreparedTypedInductive inductiveGlobalIdentity
+        <$> prepareTypedInductiveInternal
+            foundation
+            (fmap (mapSourceGlobal wrapGlobal) . resolveGlobal)
+            marker
+            inductive
+  where
+    wrapGlobal identity =
+        InductiveGlobal identity (globalType identity)
+
+prepareTypedInductiveInternal
+    :: CheckedFoundation
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
+    -> Marker
+    -> DirectInductive
+    -> Either
+        TypedInductiveError
+        (PreparedTypedInductive (InductiveGlobal global))
+prepareTypedInductiveInternal
         foundation
         resolveGlobal
         marker
@@ -261,12 +321,43 @@ prepareTypedInductive
                 <$ directInductiveParams
                     inductive)
 
+mapSourceGlobal
+    :: (left -> right)
+    -> SourceGlobal left
+    -> SourceGlobal right
+mapSourceGlobal transform (SourceGlobal identity body) =
+    SourceGlobal
+        (transform identity)
+        (mapFrozenGlobals transform <$> body)
+
+mapPreparedTypedInductive
+    :: (left -> right)
+    -> PreparedTypedInductive left
+    -> PreparedTypedInductive right
+mapPreparedTypedInductive transform
+        (PreparedTypedInductive carrierType body guards facts) =
+    PreparedTypedInductive
+        carrierType
+        (mapFrozenGlobals transform body)
+        (mapFrozenGlobals transform <$> guards)
+        (mapPreparedFact transform <$> facts)
+  where
+    mapPreparedFact mapGlobal
+            (PreparedTypedInductiveFact
+                (marker, target, rule, derivation)) =
+        PreparedTypedInductiveFact
+            ( marker
+            , mapFrozenGlobals mapGlobal target
+            , rule
+            , mapKernelDerivationGlobals mapGlobal derivation
+            )
+
 prepareCarrierBody
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> Either
         TypedInductiveError
-        (FrozenCheckedCore CheckedGlobalRef)
+        (FrozenCheckedCore (InductiveGlobal global))
 prepareCarrierBody resolveGlobal inductive = do
     body <-
         buildUnderVariables
@@ -286,17 +377,17 @@ prepareCarrierBody resolveGlobal inductive = do
     checked <-
         first TypedInductiveCoreError
             (checkCanonicalCore
-                (Just . checkedGlobalType)
+                (Just . inductiveGlobalType)
                 closed)
     pure checked
 
 prepareGuardTarget
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> DirectInductiveClause
     -> Either
         TypedInductiveError
-        (FrozenCheckedCore CheckedGlobalRef)
+        (FrozenCheckedCore (InductiveGlobal global))
 prepareGuardTarget
         resolveGlobal
         inductive
@@ -343,8 +434,8 @@ prepareGuardTarget
 
 assignGuardSources
     :: CheckedFoundation
-    -> [FrozenCheckedCore CheckedGlobalRef]
-    -> [PreparedInductiveGuard]
+    -> [FrozenCheckedCore (InductiveGlobal global)]
+    -> [PreparedInductiveGuard (InductiveGlobal global)]
 assignGuardSources foundation =
     snd . List.mapAccumL assign 0
   where
@@ -372,13 +463,13 @@ assignGuardSources foundation =
 
 prepareFacts
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> Marker
     -> DirectInductive
-    -> NonEmpty PreparedInductiveGuard
+    -> NonEmpty (PreparedInductiveGuard (InductiveGlobal global))
     -> Either
         TypedInductiveError
-        (NonEmpty PreparedTypedInductiveFact)
+        (NonEmpty (PreparedTypedInductiveFact (InductiveGlobal global)))
 prepareFacts
         foundation
         resolveGlobal
@@ -440,14 +531,14 @@ prepareFacts
 
 prepareIntroductionFact
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> Marker
     -> DirectInductive
     -> Natural
-    -> (PreparedInductiveGuard, DirectInductiveClause)
+    -> (PreparedInductiveGuard (InductiveGlobal global), DirectInductiveClause)
     -> Either
         TypedInductiveError
-        PreparedTypedInductiveFact
+        (PreparedTypedInductiveFact (InductiveGlobal global))
 prepareIntroductionFact
         foundation
         resolveGlobal
@@ -459,7 +550,7 @@ prepareIntroductionFact
         proveUnderVariables
             (rootProofContext
                 foundation
-                (Just . checkedGlobalType))
+                (Just . inductiveGlobalType))
             emptyEnvironment
             (directInductiveParams inductive
                 <> directClauseVariables clause)
@@ -699,14 +790,15 @@ prepareIntroductionFact
         (introMarker
             marker
             (clauseIndex + 1))
+        SetLfpFixed
         proof
 
 preparedGuardProof
-    :: ProofContext CheckedGlobalRef
-    -> PreparedInductiveGuard
+    :: ProofContext (InductiveGlobal global)
+    -> PreparedInductiveGuard (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 preparedGuardProof context = \case
     PreparedFoundationGuard tag ->
         first TypedInductiveProofError
@@ -717,12 +809,12 @@ preparedGuardProof context = \case
 
 prepareDomainSubsetFact
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> Marker
     -> DirectInductive
     -> Either
         TypedInductiveError
-        PreparedTypedInductiveFact
+        (PreparedTypedInductiveFact (InductiveGlobal global))
 prepareDomainSubsetFact
         foundation
         resolveGlobal
@@ -732,7 +824,7 @@ prepareDomainSubsetFact
         proveUnderVariables
             (rootProofContext
                 foundation
-                (Just . checkedGlobalType))
+                (Just . inductiveGlobalType))
             emptyEnvironment
             (directInductiveParams
                 inductive)
@@ -757,16 +849,17 @@ prepareDomainSubsetFact
                         operator))
     preparedFact
         (derivedMarker marker "dom_subset")
+        SetLfpBound
         proof
 
 prepareCasesFact
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> Marker
     -> DirectInductive
     -> Either
         TypedInductiveError
-        PreparedTypedInductiveFact
+        (PreparedTypedInductiveFact (InductiveGlobal global))
 prepareCasesFact
         foundation
         resolveGlobal
@@ -776,7 +869,7 @@ prepareCasesFact
         proveUnderVariables
             (rootProofContext
                 foundation
-                (Just . checkedGlobalType))
+                (Just . inductiveGlobalType))
             emptyEnvironment
             (directInductiveParams
                 inductive)
@@ -907,16 +1000,17 @@ prepareCasesFact
                                         predicateTarget))))
     preparedFact
         (derivedMarker marker "cases")
+        SetLfpFixed
         proof
 
 prepareInductionFact
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> Marker
     -> DirectInductive
     -> Either
         TypedInductiveError
-        PreparedTypedInductiveFact
+        (PreparedTypedInductiveFact (InductiveGlobal global))
 prepareInductionFact
         foundation
         resolveGlobal
@@ -926,7 +1020,7 @@ prepareInductionFact
         proveUnderVariables
             (rootProofContext
                 foundation
-                (Just . checkedGlobalType))
+                (Just . inductiveGlobalType))
             emptyEnvironment
             (directInductiveParams
                 inductive)
@@ -989,7 +1083,7 @@ prepareInductionFact
                                         subsetAtElement <-
                                             first TypedInductiveCoreError
                                                 (weakenScopedCore
-                                                    (Just . checkedGlobalType)
+                                                    (Just . inductiveGlobalType)
                                                     TySet
                                                     subset)
                                         predicate <-
@@ -1049,21 +1143,22 @@ prepareInductionFact
                                                 expected)))))
     preparedFact
         (derivedMarker marker "induct")
+        SetLfpInduct
         proof
 
 proveUnderVariables
-    :: ProofContext CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
     -> [VarSymbol]
-    -> ( ProofContext CheckedGlobalRef
+    -> ( ProofContext (InductiveGlobal global)
          -> InductiveEnvironment
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 proveUnderVariables context environment variables build =
     case variables of
         [] ->
@@ -1084,22 +1179,23 @@ proveUnderVariables context environment variables build =
                         build)
 
 checkedTerm
-    :: ProofContext CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (ScopedCheckedCore CheckedGlobalRef)
+        (ScopedCheckedCore (InductiveGlobal global))
 checkedTerm context =
     first TypedInductiveProofError
         . scopedTerm context
 
 preparedFact
     :: Marker
-    -> BuiltProof CheckedGlobalRef
+    -> KernelRuleTag
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        PreparedTypedInductiveFact
-preparedFact marker proof = do
+        (PreparedTypedInductiveFact (InductiveGlobal global))
+preparedFact marker rule proof = do
     target <-
         maybe
             (Left TypedInductiveProofRemainedOpen)
@@ -1110,6 +1206,7 @@ preparedFact marker proof = do
         (PreparedTypedInductiveFact
             ( marker
             , target
+            , rule
             , builtProofDerivation proof
             ))
 
@@ -1126,13 +1223,13 @@ derivedMarker (Marker marker) suffix =
         (marker <> "_" <> suffix)
 
 eliminateWrittenForalls
-    :: ProofContext CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
     -> [VarSymbol]
-    -> BuiltProof CheckedGlobalRef
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 eliminateWrittenForalls
         context
         environment
@@ -1154,16 +1251,16 @@ eliminateWrittenForalls
         variables
 
 provePremises
-    :: ProofContext CheckedGlobalRef
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> ( [BuiltProof CheckedGlobalRef]
+    :: ProofContext (InductiveGlobal global)
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> ( [BuiltProof (InductiveGlobal global)]
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 provePremises context premises build =
     case conjunctionList premises of
         Nothing ->
@@ -1183,11 +1280,11 @@ provePremises context premises build =
                     build projections)
 
 conjunctionIntroductionList
-    :: ProofContext CheckedGlobalRef
-    -> [BuiltProof CheckedGlobalRef]
+    :: ProofContext (InductiveGlobal global)
+    -> [BuiltProof (InductiveGlobal global)]
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 conjunctionIntroductionList _context [] =
     Left
         (TypedInductiveUnsupportedExpression
@@ -1204,12 +1301,12 @@ conjunctionIntroductionList context (firstProof : remaining) =
         remaining
 
 projectConjunctionList
-    :: ProofContext CheckedGlobalRef
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        [BuiltProof CheckedGlobalRef]
+        [BuiltProof (InductiveGlobal global)]
 projectConjunctionList _context [] _proof =
     pure []
 projectConjunctionList _context [_only] proof =
@@ -1244,17 +1341,17 @@ projectConjunctionList context terms proof = do
             precedingProof
 
 introduceClauseWitnesses
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> DirectInductiveClause
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 introduceClauseWitnesses
         resolveGlobal
         _inductive
@@ -1300,7 +1397,7 @@ introduceClauseWitnesses
         bodyUnderBinder <-
             first TypedInductiveCoreError
                 (checkScopedCanonicalCore
-                    (Just . checkedGlobalType)
+                    (Just . inductiveGlobalType)
                     (TySet
                         : proofContextTypes
                             context)
@@ -1314,15 +1411,15 @@ introduceClauseWitnesses
                 inner)
 
 clauseFormulaWithBinders
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductiveClause
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
     -> [VarSymbol]
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 clauseFormulaWithBinders
         resolveGlobal
         clause
@@ -1387,13 +1484,13 @@ rebindEnvironment variable
             (Map.insert variable 0 variables))
 
 injectDisjunction
-    :: ProofContext CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
     -> Natural
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> BuiltProof CheckedGlobalRef
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 injectDisjunction context index alternatives proof =
     case splitAtNatural index alternatives of
         Nothing ->
@@ -1445,13 +1542,13 @@ injectDisjunction context index alternatives proof =
                 rest
 
 closureTerms
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        [CanonicalTerm CheckedGlobalRef]
+        [CanonicalTerm (InductiveGlobal global)]
 closureTerms
         resolveGlobal
         inductive
@@ -1503,13 +1600,13 @@ closureTerms
 
 proveBoundedMonotonicity
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 proveBoundedMonotonicity
         _foundation
         resolveGlobal
@@ -1832,7 +1929,7 @@ proveBoundedMonotonicity
                                                 TypedInductiveCoreError
                                                 (weakenScopedCore
                                                     (Just
-                                                        . checkedGlobalType)
+                                                        . inductiveGlobalType)
                                                     TySet
                                                     operatorY)
                                         explicitMembershipY <-
@@ -1858,20 +1955,20 @@ proveBoundedMonotonicity
                 monotone))
 
 transformPredicateProof
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> BuiltProof CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 transformPredicateProof
         resolveGlobal
         inductive
@@ -1978,18 +2075,18 @@ transformPredicateProof
                                     alternativeY)))))
 
 transformClauseBody
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductiveClause
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 transformClauseBody
         resolveGlobal
         clause
@@ -2074,13 +2171,13 @@ transformClauseBody
             <> [equalityProof])
 
 subsetRelationHypothesis
-    :: ProofContext CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 subsetRelationHypothesis
         context
         left
@@ -2109,27 +2206,27 @@ subsetRelationHypothesis
             relationProof)
 
 eliminateClauseWitnesses
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductiveClause
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
     -> ( Natural
-         -> ProofContext CheckedGlobalRef
+         -> ProofContext (InductiveGlobal global)
          -> InductiveEnvironment
-         -> CanonicalTerm CheckedGlobalRef
-         -> CanonicalTerm CheckedGlobalRef
-         -> BuiltProof CheckedGlobalRef
+         -> CanonicalTerm (InductiveGlobal global)
+         -> CanonicalTerm (InductiveGlobal global)
+         -> BuiltProof (InductiveGlobal global)
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 eliminateClauseWitnesses
         resolveGlobal
         clause
@@ -2186,7 +2283,7 @@ eliminateClauseWitnesses
             bodyUnderBinder <-
                 first TypedInductiveCoreError
                     (checkScopedCanonicalCore
-                        (Just . checkedGlobalType)
+                        (Just . inductiveGlobalType)
                         (TySet
                             : proofContextTypes
                                 context)
@@ -2194,7 +2291,7 @@ eliminateClauseWitnesses
             targetUnderBinder <-
                 first TypedInductiveCoreError
                     (weakenScopedCore
-                        (Just . checkedGlobalType)
+                        (Just . inductiveGlobalType)
                         TySet
                         target)
             first TypedInductiveProofError
@@ -2217,20 +2314,20 @@ eliminateClauseWitnesses
                                 remaining)))
 
 eliminateDisjunctionAlternatives
-    :: ProofContext CheckedGlobalRef
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> BuiltProof CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ( ProofContext CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> BuiltProof (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ( ProofContext (InductiveGlobal global)
          -> Natural
-         -> BuiltProof CheckedGlobalRef
+         -> BuiltProof (InductiveGlobal global)
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 eliminateDisjunctionAlternatives
         initialContext
         alternatives
@@ -2279,18 +2376,18 @@ eliminateDisjunctionAlternatives
 
 proveInductionClosure
     :: CheckedFoundation
-    -> (Symbol -> Maybe SourceGlobal)
+    -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> BuiltProof CheckedGlobalRef
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 proveInductionClosure
         _foundation
         resolveGlobal
@@ -2311,19 +2408,19 @@ proveInductionClosure
             fixedPointAtElement <-
                 first TypedInductiveCoreError
                     (weakenScopedCore
-                        (Just . checkedGlobalType)
+                        (Just . inductiveGlobalType)
                         TySet
                         fixedPoint)
             operatorAtElement <-
                 first TypedInductiveCoreError
                     (weakenScopedCore
-                        (Just . checkedGlobalType)
+                        (Just . inductiveGlobalType)
                         TySet
                         operator)
             subsetAtElement <-
                 first TypedInductiveCoreError
                     (weakenScopedCore
-                        (Just . checkedGlobalType)
+                        (Just . inductiveGlobalType)
                         TySet
                         subset)
             inductionPredicate <-
@@ -2525,21 +2622,21 @@ proveInductionClosure
                             appliedPredicate)))
 
 proveInductionClause
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> Natural
     -> DirectInductiveClause
-    -> ProofContext CheckedGlobalRef
+    -> ProofContext (InductiveGlobal global)
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
-    -> [CanonicalTerm CheckedGlobalRef]
-    -> CanonicalTerm CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
+    -> [CanonicalTerm (InductiveGlobal global)]
+    -> CanonicalTerm (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 proveInductionClause
         resolveGlobal
         _inductive
@@ -2717,13 +2814,13 @@ proveInductionClause
             resultMembership)
 
 transportElementMembership
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 transportElementMembership
         context
         set
@@ -2788,14 +2885,14 @@ transportElementMembership
             sourceMembership)
 
 predicateAt
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 predicateAt
         resolveGlobal
         inductive
@@ -2811,14 +2908,14 @@ predicateAt
             result
 
 clauseFormulaTerms
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        [CanonicalTerm CheckedGlobalRef]
+        [CanonicalTerm (InductiveGlobal global)]
 clauseFormulaTerms
         resolveGlobal
         inductive
@@ -2836,14 +2933,14 @@ clauseFormulaTerms
                 inductive))
 
 clauseFormulaAt
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
+    -> CanonicalTerm (InductiveGlobal global)
     -> DirectInductiveClause
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 clauseFormulaAt
         resolveGlobal
         environment
@@ -2918,16 +3015,16 @@ extendVariables =
                 remaining
 
 membershipPredicate
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (ScopedCheckedCore CheckedGlobalRef)
+        (ScopedCheckedCore (InductiveGlobal global))
 membershipPredicate context set = do
     weakenedSet <-
         first TypedInductiveCoreError
             (weakenScopedCore
-                (Just . checkedGlobalType)
+                (Just . inductiveGlobalType)
                 TySet
                 set)
     checkedTerm context
@@ -2938,13 +3035,13 @@ membershipPredicate context set = do
                     weakenedSet)))
 
 operatorPredicateAt
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 operatorPredicateAt
         resolveGlobal
         inductive
@@ -2965,13 +3062,13 @@ operatorPredicateAt
     pure (CLam TySet body)
 
 separationSetAt
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 separationSetAt
         resolveGlobal
         inductive
@@ -2996,12 +3093,12 @@ separationSetAt
             predicate)
 
 foundationInstance
-    :: ProofContext CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
     -> FoundationAxiomTag
-    -> [ScopedCheckedCore CheckedGlobalRef]
+    -> [ScopedCheckedCore (InductiveGlobal global)]
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 foundationInstance context tag arguments = do
     initial <-
         first TypedInductiveProofError
@@ -3017,14 +3114,14 @@ foundationInstance context tag arguments = do
         arguments
 
 separationForward
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 separationForward
         context
         domain
@@ -3043,15 +3140,15 @@ separationForward
             membership)
 
 separationBackward
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 separationBackward
         context
         domain
@@ -3093,13 +3190,13 @@ separationBackward
             conjunction)
 
 transportMembership
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
-    -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
+    -> BuiltProof (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 transportMembership
         context
         element
@@ -3118,7 +3215,7 @@ transportMembership
     weakenedElement <-
         first TypedInductiveCoreError
             (weakenScopedCore
-                (Just . checkedGlobalType)
+                (Just . inductiveGlobalType)
                 TySet
                 element)
     function <-
@@ -3168,19 +3265,19 @@ transportMembership
             targetMembership)
 
 proveSubset
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ( ProofContext CheckedGlobalRef
-         -> ScopedCheckedCore CheckedGlobalRef
-         -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ( ProofContext (InductiveGlobal global)
+         -> ScopedCheckedCore (InductiveGlobal global)
+         -> BuiltProof (InductiveGlobal global)
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 proveSubset context left right proveElement =
     forallIntroductionTyped
         context
@@ -3189,13 +3286,13 @@ proveSubset context left right proveElement =
                 left' <-
                     first TypedInductiveCoreError
                         (weakenScopedCore
-                            (Just . checkedGlobalType)
+                            (Just . inductiveGlobalType)
                             TySet
                             left)
                 right' <-
                     first TypedInductiveCoreError
                         (weakenScopedCore
-                            (Just . checkedGlobalType)
+                            (Just . inductiveGlobalType)
                             TySet
                             right)
                 memberLeft <-
@@ -3238,17 +3335,17 @@ typedAsProofError = \case
             (Text.pack (show err))
 
 implicationIntroductionTyped
-    :: ProofContext CheckedGlobalRef
-    -> ScopedCheckedCore CheckedGlobalRef
-    -> ( ProofContext CheckedGlobalRef
-         -> BuiltProof CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
+    -> ScopedCheckedCore (InductiveGlobal global)
+    -> ( ProofContext (InductiveGlobal global)
+         -> BuiltProof (InductiveGlobal global)
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 implicationIntroductionTyped context premise build =
     first TypedInductiveProofError
         (implicationIntroductionProof
@@ -3259,17 +3356,17 @@ implicationIntroductionTyped context premise build =
                     (build extended proof)))
 
 forallIntroductionTyped
-    :: ProofContext CheckedGlobalRef
+    :: ProofContext (InductiveGlobal global)
     -> CoreType
-    -> ( ProofContext CheckedGlobalRef
-         -> ScopedCheckedCore CheckedGlobalRef
+    -> ( ProofContext (InductiveGlobal global)
+         -> ScopedCheckedCore (InductiveGlobal global)
          -> Either
             TypedInductiveError
-            (BuiltProof CheckedGlobalRef)
+            (BuiltProof (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (BuiltProof CheckedGlobalRef)
+        (BuiltProof (InductiveGlobal global))
 forallIntroductionTyped context binderType build =
     first TypedInductiveProofError
         (forallIntroductionProof
@@ -3279,21 +3376,17 @@ forallIntroductionTyped context binderType build =
                 first typedAsProofError
                     (build extended variable)))
 
-data SourceGlobal = SourceGlobal
-    !CheckedGlobalRef
-    !(Maybe (FrozenCheckedCore CheckedGlobalRef))
-
 buildUnderVariables
     :: InductiveEnvironment
     -> [VarSymbol]
     -> ( InductiveEnvironment
          -> Either
             TypedInductiveError
-            (CanonicalTerm CheckedGlobalRef)
+            (CanonicalTerm (InductiveGlobal global))
        )
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 buildUnderVariables
         environment
         []
@@ -3313,12 +3406,12 @@ buildUnderVariables
         build
 
 fixedPointTerm
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 fixedPointTerm resolveGlobal inductive environment = do
     domain <-
         lowerTerm
@@ -3339,12 +3432,12 @@ fixedPointTerm resolveGlobal inductive environment = do
             operator)
 
 operatorTerm
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> DirectInductive
     -> InductiveEnvironment
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 operatorTerm resolveGlobal inductive parameterEnvironment = do
     candidateEnvironment <-
         shiftEnvironment parameterEnvironment
@@ -3375,12 +3468,12 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do
                             clauses)))))
 
 clausePredicateTerm
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> InductiveEnvironment
     -> DirectInductiveClause
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 clausePredicateTerm
         resolveGlobal
         resultEnvironment
@@ -3429,13 +3522,13 @@ clausePredicateTerm
                             result]))))
 
 conditionTerm
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> InductiveEnvironment
-    -> CanonicalTerm CheckedGlobalRef
+    -> CanonicalTerm (InductiveGlobal global)
     -> DirectInductiveCondition
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 conditionTerm resolveGlobal environment candidate = \case
     DirectSideCondition formula ->
         lowerFormula
@@ -3462,12 +3555,12 @@ shiftEnvironment
             (succ <$> variables))
 
 lowerFormula
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> InductiveEnvironment
     -> Formula
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 lowerFormula resolveGlobal environment = \case
     IsElementOf _location element set ->
         memberTerm
@@ -3542,12 +3635,12 @@ lowerFormula resolveGlobal environment = \case
                 "quantified and higher-order side conditions are not supported by the typed inductive slice")
 
 lowerTerm
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> InductiveEnvironment
     -> Term
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 lowerTerm resolveGlobal environment = \case
     TermVar variable ->
         lookupEnvironment
@@ -3613,13 +3706,13 @@ lowerTerm resolveGlobal environment = \case
                 "higher-order source terms are not supported by the typed inductive slice")
 
 lowerApplication
-    :: (Symbol -> Maybe SourceGlobal)
+    :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
     -> InductiveEnvironment
     -> Symbol
     -> [Expr]
     -> Either
         TypedInductiveError
-        (CanonicalTerm CheckedGlobalRef)
+        (CanonicalTerm (InductiveGlobal global))
 lowerApplication resolveGlobal environment symbol arguments = do
     SourceGlobal reference body <-
         maybe
@@ -3826,14 +3919,14 @@ atNatural index (_value : rest) =
     atNatural (index - 1) rest
 
 freezeClosedTarget
-    :: CanonicalTerm CheckedGlobalRef
+    :: CanonicalTerm (InductiveGlobal global)
     -> Either
         TypedInductiveError
-        (FrozenCheckedCore CheckedGlobalRef)
+        (FrozenCheckedCore (InductiveGlobal global))
 freezeClosedTarget =
     first TypedInductiveCoreError
         . checkCanonicalCore
-            (Just . checkedGlobalType)
+            (Just . inductiveGlobalType)
 
 powerSetSymbol :: FunctionSymbol
 powerSetSymbol =
diff --git a/source/Test/Unit/Kernel.hs b/source/Test/Unit/Kernel.hs
index 310c113..27f92b2 100644
--- a/source/Test/Unit/Kernel.hs
+++ b/source/Test/Unit/Kernel.hs
@@ -438,6 +438,7 @@ replaysDirectInductiveFacts = do
         prepared <-
             expectRight
                 (Inductive.prepareTypedInductive
+                    checkedGlobalType
                     foundation
                     (const Nothing)
                     (Internal.Marker "direct_inductive")
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 1b7d36f..c299df0 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -9,11 +9,13 @@ import Checking.Backend.Problem qualified as Backend
 import Checking.Core qualified as Core
 import Checking.Declaration qualified as Declaration
 import Checking.Exact qualified as Exact
+import Checking.Exact.Inductive qualified as ExactInductive
 import Checking.Exact.Proof qualified as ExactProof
 import Checking.Foundation qualified as Foundation
 import Checking.Identity qualified as Identity
 import Checking.Module qualified as Module
 import Checking.Semantic qualified as Semantic
+import Checking.Typed.Inductive qualified as TypedInductive
 import CommandLine qualified
 import Felix.Module
 import Felix.Math.Codec
@@ -79,6 +81,10 @@ unitTests =
             compilesExactReplacementComprehensions
         , testCase "compiles and reuses exact finite sets"
             compilesAndReusesExactFiniteSets
+        , testCase "prepares exact direct inductives"
+            preparesExactDirectInductives
+        , testCase "rejects nested exact inductive recursion"
+            rejectsNestedExactInductiveRecursion
         , testCase "reuses exact separation validation"
             reusesExactSeparationValidation
         , testCase "compiles exact source axioms"
@@ -982,6 +988,82 @@ compilesAndReusesExactFiniteSets =
                     (Declaration.pendingModulePrefixCurrent
                         (Module.sealedTypedModulePrefix warm))
 
+preparesExactDirectInductives :: Assertion
+preparesExactDirectInductives = do
+    prepared <-
+        expectRight
+            =<< prepareExactInductiveFixture
+                "test/phase5/exact-inductive.tex"
+    assertEqual "exact inductive carrier type"
+        (Core.TyArrow Core.TySet Core.TySet)
+        (ExactInductive.preparedExactInductiveCarrierType prepared)
+    assertEqual "exact inductive carrier body"
+        expectedCarrier
+        (Core.frozenCoreTerm
+            (ExactInductive.preparedExactInductiveCarrierBody prepared))
+    assertEqual "foundation guard needs no imported fact"
+        []
+        (Vector.toList
+            (ExactInductive.preparedExactInductiveGuardTargets prepared))
+    let facts =
+            toList
+                (ExactInductive.preparedExactInductiveFacts prepared)
+    assertEqual "generated fact order"
+        [ Raw.Marker "phase5_fin_intro_1"
+        , Raw.Marker "phase5_fin_dom_subset"
+        , Raw.Marker "phase5_fin_cases"
+        , Raw.Marker "phase5_fin_induct"
+        ]
+        (TypedInductive.typedInductiveFactMarker <$> facts)
+    assertEqual "generated guarded-rule descriptors"
+        [ Foundation.SetLfpFixed
+        , Foundation.SetLfpBound
+        , Foundation.SetLfpFixed
+        , Foundation.SetLfpInduct
+        ]
+        (TypedInductive.typedInductiveFactRule <$> facts)
+    assertBool "generated targets are closed propositions"
+        (all
+            (\fact ->
+                let target = TypedInductive.typedInductiveFactTarget fact
+                in Core.frozenCoreType target == Core.TyProp
+                    && Set.null (Core.frozenCoreGlobals target))
+            facts)
+  where
+    apply1 intrinsic argument =
+        Core.CApp (Core.CIntrinsic intrinsic) argument
+    expectedCarrier =
+        Core.CLam Core.TySet
+            (Core.CApp
+                (Core.CApp
+                    (Core.CIntrinsic Core.ISetLfp)
+                    (apply1 Core.UnivOf (Core.CBound 0)))
+                (Core.CLam Core.TySet
+                    (Core.CApp
+                        (Core.CApp
+                            (Core.CIntrinsic Core.Sep)
+                            (apply1 Core.UnivOf (Core.CBound 1)))
+                        (Core.CLam Core.TySet
+                            (Core.CEq Core.TySet
+                                (Core.CBound 0)
+                                (Core.CBound 2))))))
+
+rejectsNestedExactInductiveRecursion :: Assertion
+rejectsNestedExactInductiveRecursion = do
+    result <-
+        prepareExactInductiveFixture
+            "test/phase5/exact-inductive-nested.tex"
+    case result of
+        Left (ExactInductive.ExactInductiveNestedRecursion location) ->
+            assertEqual "nested recursive occurrence line"
+                6
+                (locLine location)
+        Left failure ->
+            assertFailure
+                ("unexpected exact inductive failure: " <> show failure)
+        Right{} ->
+            assertFailure "nested inductive recursion was accepted"
+
 assertExactFiniteSetModule
     :: String
     -> Module.SealedTypedModule
@@ -2518,6 +2600,71 @@ countingAcceptedResolver executable runs =
                     Provers.defaultMemoryLimit)
                 prepared)
 
+prepareExactInductiveFixture
+    :: FilePath
+    -> IO
+        (Either
+            ExactInductive.ExactInductiveError
+            ExactInductive.PreparedExactInductive)
+prepareExactInductiveFixture relative = do
+    root <- getCurrentDirectory
+    foundation <- expectRight Foundation.checkedFoundation
+    bootstrap <-
+        expectRight
+            =<< Module.buildBootstrapPreludeSession
+                foundation
+                unusedResolver
+    mounts <- exactFixtureMounts root
+    workspace <- parseExactWorkspace bootstrap mounts relative
+    parsed <-
+        sole "exact inductive parsed module"
+            (toList
+                (Parse.parsedWorkspaceImportedBeforeImporter workspace))
+    let identified = Module.identifiedPhysicalModule parsed
+        owner = Module.identifiedModuleOwner identified
+        parsedModule = Module.identifiedModuleParsed identified
+    block <-
+        sole "exact inductive block"
+            (Parse.identifiedParsedModuleBlocks parsedModule)
+    let entries =
+            [ Parse.parsedSyntaxOccurrenceEntry occurrence
+            | occurrence <-
+                Parse.identifiedParsedModuleSyntaxOccurrences parsedModule
+            , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == 0
+            ]
+        action
+            :: Declaration.ModuleDriver Void
+                (Either
+                    ExactInductive.ExactInductiveError
+                    ExactInductive.PreparedExactInductive)
+        action =
+            ExactInductive.prepareExactInductive
+                foundation
+                block
+                entries
+    result <-
+        Declaration.runModuleDriver
+            foundation
+            owner
+            []
+            unusedResolver
+            Declaration.FreshValidation
+            action
+    driver <- expectRight result
+    case driver of
+        Declaration.DriverSucceeded prepared _semantic _prefix _closure ->
+            pure prepared
+        Declaration.DriverFailed failure _prefix ->
+            assertFailure
+                ("exact inductive preparation driver failed: "
+                    <> show failure)
+                >> fail "unreachable"
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure
+                ("exact inductive preparation driver did not seal: "
+                    <> show failure)
+                >> fail "unreachable"
+
 compileExactFixture
     :: FilePath
     -> IO
author	adelon <22380201+adelon@users.noreply.github.com>	2026-08-02 02:33:14 +0200
committer	adelon <22380201+adelon@users.noreply.github.com>	2026-08-02 02:33:14 +0200
commit	d55d2416bc4f6a9aa055a17deae4fba0fe906316 (patch)
tree	4a248850088bc0aad1b5084062abc385008d6d87 /source
parent	118fd4a72f01ebfcedd2c75c2f34cc46e9692586 (diff)