diff options
Diffstat (limited to 'source/Test/Unit/Kernel.hs')
| -rw-r--r-- | source/Test/Unit/Kernel.hs | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/source/Test/Unit/Kernel.hs b/source/Test/Unit/Kernel.hs index 27f92b2..c24debf 100644 --- a/source/Test/Unit/Kernel.hs +++ b/source/Test/Unit/Kernel.hs @@ -9,7 +9,6 @@ import Checking.Foundation qualified as Foundation import Checking.Kernel.Derivation import Checking.Kernel.Semantics qualified as Semantics import Checking.Kernel.SetLfp qualified as SetLfp -import Checking.Transition (checkedGlobalType) import Checking.Typed.Inductive qualified as Inductive import Report.Location (pattern Nowhere) import Syntax.Internal qualified as Internal @@ -23,6 +22,9 @@ import Test.Tasty.HUnit data TestGlobal = TestGlobal deriving (Show, Eq, Ord) +testGlobalType :: TestGlobal -> CoreType +testGlobalType _global = TySet + unitTests :: TestTree unitTests = testGroup "Kernel replay" @@ -438,7 +440,7 @@ replaysDirectInductiveFacts = do prepared <- expectRight (Inductive.prepareTypedInductive - checkedGlobalType + testGlobalType foundation (const Nothing) (Internal.Marker "direct_inductive") @@ -455,7 +457,7 @@ replaysDirectInductiveFacts = do (replayKernelDerivation foundation defaultKernelReplayLimits - (Just . checkedGlobalType) + (const Nothing) imports (Inductive.typedInductiveFactTarget fact) |