diff --git a/primer-api/primer-api.cabal b/primer-api/primer-api.cabal
index 3c2f4fb81..190768d7b 100644
--- a/primer-api/primer-api.cabal
+++ b/primer-api/primer-api.cabal
@@ -156,6 +156,7 @@ test-suite primer-api-test
     , stm-containers
     , tasty                   ^>=1.5
     , tasty-discover
+    , tasty-expected-failure  ^>=0.12.3
     , tasty-golden            ^>=2.3.5
     , tasty-hunit
     , text
diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs
index c6b0c3c43..212495c95 100644
--- a/primer-api/test/Tests/API.hs
+++ b/primer-api/test/Tests/API.hs
@@ -9,6 +9,9 @@ import Data.Text.Lazy qualified as TL
 import Hedgehog hiding (Property, Var, property)
 import Optics ((.~))
 import Primer.API (
+  EvalBoundedInterpResp (..),
+  EvalFullResp (..),
+  EvalInterpResp (..),
   NewSessionReq (..),
   OkOrMismatch (Mismatch, Ok, expected, got),
   PrimerErr,
@@ -18,8 +21,12 @@ import Primer.API (
   copySession,
   deleteSession,
   edit,
+  evalBoundedInterp,
   evalBoundedInterp',
+  evalFull,
   evalFull',
+  evalInterp,
+  evalInterp',
   findSessions,
   flushSessions,
   getApp,
@@ -61,7 +68,18 @@ import Primer.App (
   Selection' (SelectionDef),
   newApp,
  )
-import Primer.Builtins (cTrue, cZero, tBool, tList, tMaybe, tNat)
+import Primer.App qualified as App
+import Primer.Builtins (
+  cCons,
+  cFalse,
+  cNil,
+  cTrue,
+  cZero,
+  tBool,
+  tList,
+  tMaybe,
+  tNat,
+ )
 import Primer.Core
 import Primer.Core.DSL hiding (app)
 import Primer.Core.Utils (forgetMetadata, forgetTypeMetadata)
@@ -73,13 +91,18 @@ import Primer.Database (
   fromSessionName,
  )
 import Primer.Def (astDefExpr, astDefType, defAST)
-import Primer.Eval (NormalOrderOptions (UnderBinders))
+import Primer.Eval (
+  Dir (Chk),
+  NormalOrderOptions (UnderBinders),
+ )
 import Primer.EvalFullInterp (
   Timeout (MicroSec),
  )
 import Primer.Examples (
   comprehensive,
   even3App,
+  mapOddApp,
+  mapOddPrimApp,
  )
 import Primer.Gen.Core.Raw (evalExprGen, genExpr, genType)
 import Primer.Module (moduleDefsQualified)
@@ -91,6 +114,7 @@ import Primer.Test.Util (
   assertException,
   constructSaturatedCon,
   constructTCon,
+  gvn,
   (@?=),
  )
 import Primer.UUIDv4 (nextRandom)
@@ -100,6 +124,9 @@ import Tasty (
   property,
  )
 import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.ExpectedFailure (
+  expectFailBecause,
+ )
 import Test.Tasty.Golden (goldenVsString)
 import Test.Tasty.HUnit hiding ((@?=))
 import Text.Pretty.Simple (pShowNoColor)
@@ -483,6 +510,279 @@ test_renameSession_too_long =
       step "it should be truncated at 64 characters"
       name @?= toS (replicate 64 'a')
 
+test_evalFull_even3 :: TestTree
+test_evalFull_even3 =
+  testCaseSteps "evalFull even3" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the even3App to the session"
+      sid <- addSession "even3App" even3App
+      step "Eval even3"
+      let expr = create' $ gvar $ gvn ["Even3"] "even 3?"
+      resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders)
+      let expected = create' $ con0 cFalse
+      case resp of
+        Left e -> liftIO $ assertFailure $ "ProgError: " <> show e
+        Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e
+        Right (App.EvalFullRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+test_evalFull_mapOdd :: TestTree
+test_evalFull_mapOdd =
+  testCaseSteps "evalFull mapOdd" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddApp to the session"
+      sid <- addSession "mapOddApp" mapOddApp
+      step "Eval mapOdd"
+      let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd"
+      resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders)
+      let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        Left e -> liftIO $ assertFailure $ "ProgError: " <> show e
+        Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e
+        Right (App.EvalFullRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+test_evalFull_mapOddPrim :: TestTree
+test_evalFull_mapOddPrim =
+  testCaseSteps "evalFull mapOddPrim" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddPrimApp to the session"
+      sid <- addSession "mapOddPrimApp" mapOddPrimApp
+      step "Eval mapOdd"
+      let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd"
+      resp <- evalFull sid (App.EvalFullReq expr Chk 1000 UnderBinders)
+      let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        Left e -> liftIO $ assertFailure $ "ProgError: " <> show e
+        Right (App.EvalFullRespTimedOut e) -> liftIO $ assertFailure $ "timed out: " <> show e
+        Right (App.EvalFullRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+test_evalFull'_even3 :: TestTree
+test_evalFull'_even3 =
+  testCaseSteps "evalFull' even3" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the even3App to the session"
+      sid <- addSession "even3App" even3App
+      step "Eval even3"
+      resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["Even3"] "even 3?"
+      let expected = viewTreeExpr $ create' $ con0 cFalse
+      case resp of
+        EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e
+        EvalFullRespNormal e -> zTIds e @?= zTIds expected
+
+test_evalFull'_mapOdd :: TestTree
+test_evalFull'_mapOdd =
+  testCaseSteps "evalFull' mapOdd" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddApp to the session"
+      sid <- addSession "mapOddApp" mapOddApp
+      step "Eval mapOdd"
+      resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["MapOdd"] "mapOdd"
+      let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e
+        EvalFullRespNormal e -> zTIds e @?= zTIds expected
+
+test_evalFull'_mapOddPrim :: TestTree
+test_evalFull'_mapOddPrim =
+  testCaseSteps "evalFull' mapOddPrim" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddPrimApp to the session"
+      sid <- addSession "mapOddPrimApp" mapOddPrimApp
+      step "Eval mapOdd"
+      resp <- evalFull' sid (Just 1000) (Just UnderBinders) $ gvn ["MapOdd"] "mapOdd"
+      let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        EvalFullRespTimedOut e -> liftIO $ assertFailure $ "timed out: " <> show e
+        EvalFullRespNormal e -> zTIds e @?= zTIds expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalInterp_even3 :: TestTree
+test_evalInterp_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalInterp even3" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the even3App to the session"
+      sid <- addSession "even3App" even3App
+      step "Eval even3"
+      let expr = create' $ gvar $ gvn ["Even3"] "even 3?"
+      resp <- evalInterp sid $ App.EvalInterpReq expr Chk
+      let expected = create' $ con0 cFalse
+      case resp of
+        Left e -> liftIO $ assertFailure $ "ProgError: " <> show e
+        Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalInterp_mapOdd :: TestTree
+test_evalInterp_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalInterp mapOdd" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddApp to the session"
+      sid <- addSession "mapOddApp" mapOddApp
+      step "Eval mapOdd"
+      let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd"
+      resp <- evalInterp sid $ App.EvalInterpReq expr Chk
+      let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        Left e -> liftIO $ assertFailure $ "ProgError: " <> show e
+        Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalInterp_mapOddPrim :: TestTree
+test_evalInterp_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalInterp mapOddPrim" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddPrimApp to the session"
+      sid <- addSession "mapOddPrimApp" mapOddPrimApp
+      step "Eval mapOdd"
+      let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd"
+      resp <- evalInterp sid $ App.EvalInterpReq expr Chk
+      let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        Left e -> liftIO $ assertFailure $ "ProgError: " <> show e
+        Right (App.EvalInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalInterp'_even3 :: TestTree
+test_evalInterp'_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalInterp' even3" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the even3App to the session"
+      sid <- addSession "even3App" even3App
+      step "Eval even3"
+      (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["Even3"] "even 3?"
+      let expected = viewTreeExpr $ create' $ con0 cFalse
+      zTIds e @?= zTIds expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalInterp'_mapOdd :: TestTree
+test_evalInterp'_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalInterp' mapOdd" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddApp to the session"
+      sid <- addSession "mapOddApp" mapOddApp
+      step "Eval mapOdd"
+      (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["MapOdd"] "mapOdd"
+      let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      zTIds e @?= zTIds expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalInterp'_mapOddPrim :: TestTree
+test_evalInterp'_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalInterp' mapOddPrim" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddPrimApp to the session"
+      sid <- addSession "mapOddPrimApp" mapOddPrimApp
+      step "Eval mapOdd"
+      (EvalInterpRespNormal e) <- evalInterp' sid $ gvn ["MapOdd"] "mapOdd"
+      let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      zTIds e @?= zTIds expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalBoundedInterp_even3 :: TestTree
+test_evalBoundedInterp_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalBoundedInterp even3" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the even3App to the session"
+      sid <- addSession "even3App" even3App
+      step "Eval even3"
+      let expr = create' $ gvar $ gvn ["Even3"] "even 3?"
+      resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000)
+      let expected = create' $ con0 cFalse
+      case resp of
+        Left err -> liftIO $ assertFailure $ "ProgError: " <> show err
+        Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err
+        Right (App.EvalBoundedInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalBoundedInterp_mapOdd :: TestTree
+test_evalBoundedInterp_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalBoundedInterp mapOdd" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddApp to the session"
+      sid <- addSession "mapOddApp" mapOddApp
+      step "Eval mapOdd"
+      let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd"
+      resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000)
+      let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        Left err -> liftIO $ assertFailure $ "ProgError: " <> show err
+        Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err
+        Right (App.EvalBoundedInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalBoundedInterp_mapOddPrim :: TestTree
+test_evalBoundedInterp_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalBoundedInterp mapOddPrim" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddPrimApp to the session"
+      sid <- addSession "mapOddPrimApp" mapOddPrimApp
+      step "Eval mapOdd"
+      let expr = create' $ gvar $ gvn ["MapOdd"] "mapOdd"
+      resp <- evalBoundedInterp sid (App.EvalBoundedInterpReq expr Chk $ MicroSec 10_000)
+      let expected = create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        Left err -> liftIO $ assertFailure $ "ProgError: " <> show err
+        Right (App.EvalBoundedInterpRespFailed err) -> liftIO $ assertFailure $ "InterpError: " <> show err
+        Right (App.EvalBoundedInterpRespNormal e) -> forgetMetadata e @?= forgetMetadata expected
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalBoundedInterp'_even3 :: TestTree
+test_evalBoundedInterp'_even3 = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalBoundedInterp' even3" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the even3App to the session"
+      sid <- addSession "even3App" even3App
+      step "Eval even3"
+      resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["Even3"] "even 3?"
+      let expected = viewTreeExpr $ create' $ con0 cFalse
+      case resp of
+        EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected
+        e -> liftIO $ assertFailure $ show e
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalBoundedInterp'_mapOdd :: TestTree
+test_evalBoundedInterp'_mapOdd = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalBoundedInterp' mapOdd" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddApp to the session"
+      sid <- addSession "mapOddApp" mapOddApp
+      step "Eval mapOdd"
+      resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["MapOdd"] "mapOdd"
+      let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected
+        e -> liftIO $ assertFailure $ show e
+
+-- https://github.com/hackworthltd/primer/issues/1247
+test_evalBoundedInterp'_mapOddPrim :: TestTree
+test_evalBoundedInterp'_mapOddPrim = expectFailBecause "interpreter can't reduce top-level definitions" $ do
+  testCaseSteps "evalBoundedInterp' mapOddPrim" $ \step' -> do
+    runAPI $ do
+      let step = liftIO . step'
+      step "Add the mapOddPrimApp to the session"
+      sid <- addSession "mapOddPrimApp" mapOddPrimApp
+      step "Eval mapOdd"
+      resp <- evalBoundedInterp' sid (Just $ MicroSec 10_000) $ gvn ["MapOdd"] "mapOdd"
+      let expected = viewTreeExpr $ create' $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+      case resp of
+        EvalBoundedInterpRespNormal e -> zTIds e @?= zTIds expected
+        e -> liftIO $ assertFailure $ show e
+
 test_eval_undo :: TestTree
 test_eval_undo =
   testCaseSteps "eval plays nicely with undo/redo" $ \step' -> do
@@ -740,6 +1040,9 @@ test_selectioninfo =
                 }
           )
 
+zTIds :: Tree -> Tree
+zTIds = treeIds .~ "0"
+
 zeroTKIds :: TypeOrKind -> TypeOrKind
 zeroTKIds = \case
   Type om -> Type $ zOMIds om
@@ -749,5 +1052,3 @@ zeroTKIds = \case
     zOMIds = \case
       Ok t -> Ok $ zTIds t
       Mismatch t1 t2 -> Mismatch (zTIds t1) (zTIds t2)
-    zTIds :: Tree -> Tree
-    zTIds = treeIds .~ "0"
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 5e281b14b..6d1df4411 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -35,6 +35,8 @@ module Primer.App (
   newEmptyProg',
   newProg,
   newProg',
+  allDefs,
+  allTypes,
   progAllModules,
   progAllDefs,
   progAllTypeDefs,
diff --git a/primer/src/Primer/Examples.hs b/primer/src/Primer/Examples.hs
index 57515df10..be4ff1878 100644
--- a/primer/src/Primer/Examples.hs
+++ b/primer/src/Primer/Examples.hs
@@ -40,6 +40,7 @@ module Primer.Examples (
   -- * Toy 'App's.
   even3App,
   mapOddApp,
+  mapOddPrimApp,
 ) where
 
 import Foreword hiding (
@@ -544,3 +545,9 @@ mapOddApp :: App
 mapOddApp =
   let (p, id_, nc) = mapOddProg 4
    in mkApp id_ nc p
+
+-- | An 'App' containing 'mapOddPrimProg'.
+mapOddPrimApp :: App
+mapOddPrimApp =
+  let (p, id_, nc) = mapOddPrimProg 4
+   in mkApp id_ nc p
diff --git a/primer/test/Tests/EvalFullInterp.hs b/primer/test/Tests/EvalFullInterp.hs
index ab5bdcd9c..bbb614f60 100644
--- a/primer/test/Tests/EvalFullInterp.hs
+++ b/primer/test/Tests/EvalFullInterp.hs
@@ -895,9 +895,44 @@ unit_prim_partial_map =
         s <- evalFullTest builtinTypes (gs <> prims) Syn e
         s @?= Right r
 
+-- https://github.com/hackworthltd/primer/issues/1247
+
+-- unit_interp_even3 :: Assertion
+-- unit_interp_even3 =
+--   let (prog, _, _) = even3Prog
+--       types = allTypes prog
+--       defs = allDefs prog
+--       expr = create1 $ gvar $ gvn ["Even3"] "even 3?"
+--       expect = create1 $ con0 cFalse
+--    in do
+--         s <- evalFullTest types defs Chk expr
+--         s @?= Right expect
+
+-- unit_interp_mapOdd2 :: Assertion
+-- unit_interp_mapOdd2 =
+--   let (prog, _, _) = mapOddProg 2
+--       types = allTypes prog
+--       defs = allDefs prog
+--       expr = create1 $ gvar $ gvn ["MapOdd"] "mapOdd"
+--       expect = create1 $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]
+--    in do
+--         s <- evalFullTest types defs Chk expr
+--         s @?= Right expect
+
+-- unit_interp_mapOddPrim2 :: Assertion
+-- unit_interp_mapOddPrim2 =
+--   let (prog, _, _) = mapOddPrimProg 2
+--       types = allTypes prog
+--       defs = allDefs prog
+--       expr = create1 $ gvar $ gvn ["MapOdd"] "mapOdd"
+--       expect = create1 $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]
+--    in do
+--         s <- evalFullTest types defs Chk expr
+--         s @?= Right expect
+
 -- Test that 'handleEvalInterpRequest' will reduce imported terms
-unit_eval_interp_full_modules :: Assertion
-unit_eval_interp_full_modules =
+unit_handleEvalInterpRequest_modules :: Assertion
+unit_handleEvalInterpRequest_modules =
   let test = do
         builtinModule' <- builtinModule
         primitiveModule' <- primitiveModule
@@ -918,8 +953,8 @@ unit_eval_interp_full_modules =
         Right assertion -> assertion
 
 -- Test that 'handleEvalBoundedInterpRequest' will reduce imported terms
-unit_eval_interp_full_modules_bounded :: Assertion
-unit_eval_interp_full_modules_bounded =
+unit_handleEvalBoundedInterpRequest_modules :: Assertion
+unit_handleEvalBoundedInterpRequest_modules =
   let test = do
         builtinModule' <- builtinModule
         primitiveModule' <- primitiveModule
@@ -942,10 +977,65 @@ unit_eval_interp_full_modules_bounded =
         Left err -> assertFailure $ show err
         Right assertion -> assertion
 
+-- https://github.com/hackworthltd/primer/issues/1247
+
+-- unit_handleEvalInterpRequest_even3 :: Assertion
+-- unit_handleEvalInterpRequest_even3 =
+--   let test = do
+--         expr <- gvar $ gvn ["Even3"] "even 3?"
+--         (EvalInterpRespNormal e) <-
+--           readerToState
+--             $ handleEvalInterpRequest
+--             $ EvalInterpReq
+--               { expr = expr
+--               , dir = Chk
+--               }
+--         expect <- con0 cFalse
+--         pure $ e ~= expect
+--    in runAppTestM even3App test <&> fst >>= \case
+--         Left err -> assertFailure $ show err
+--         Right assertion -> assertion
+
+-- unit_handleEvalInterpRequest_mapOdd :: Assertion
+-- unit_handleEvalInterpRequest_mapOdd =
+--   let test = do
+--         expr <- gvar $ gvn ["MapOdd"] "mapOdd"
+--         (EvalInterpRespNormal e) <-
+--           readerToState
+--             $ handleEvalInterpRequest
+--             $ EvalInterpReq
+--               { expr = expr
+--               , dir = Chk
+--               }
+--         -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3]
+--         expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+--         pure $ e ~= expect
+--    in runAppTestM mapOddApp test <&> fst >>= \case
+--         Left err -> assertFailure $ show err
+--         Right assertion -> assertion
+
+-- unit_handleEvalInterpRequest_mapOddPrim :: Assertion
+-- unit_handleEvalInterpRequest_mapOddPrim =
+--   let test = do
+--         expr <- gvar $ gvn ["MapOdd"] "mapOdd"
+--         (EvalInterpRespNormal e) <-
+--           readerToState
+--             $ handleEvalInterpRequest
+--             $ EvalInterpReq
+--               { expr = expr
+--               , dir = Chk
+--               }
+--         -- Note that the 'mapOddPrimApp' includes a program runs @mapOdd@ over a list of [0..3]
+--         expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+--         pure $ e ~= expect
+--    in runAppTestM mapOddPrimApp test <&> fst >>= \case
+--         Left err -> assertFailure $ show err
+--         Right assertion -> assertion
+
 -- Test that 'handleEvalInterpRequest' will reduce case analysis of
 -- imported types
-unit_eval_interp_full_modules_scrutinize_imported_type :: Assertion
-unit_eval_interp_full_modules_scrutinize_imported_type =
+unit_handleEvalInterpRequest_modules_scrutinize_imported_type :: Assertion
+unit_handleEvalInterpRequest_modules_scrutinize_imported_type =
   let test = do
         m' <- m
         importModules [m']
@@ -978,8 +1068,8 @@ unit_eval_interp_full_modules_scrutinize_imported_type =
 
 -- Test that 'handleEvalBoundedInterpRequest' will reduce case analysis
 -- of imported types
-unit_eval_interp_full_modules_scrutinize_imported_type_bounded :: Assertion
-unit_eval_interp_full_modules_scrutinize_imported_type_bounded =
+unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type :: Assertion
+unit_handleEvalBoundedInterpRequest_modules_scrutinize_imported_type =
   let test = do
         m' <- m
         importModules [m']
@@ -1013,9 +1103,73 @@ unit_eval_interp_full_modules_scrutinize_imported_type_bounded =
           , moduleDefs = mempty
           }
 
+-- https://github.com/hackworthltd/primer/issues/1247
+
+-- unit_handleEvalBoundedInterpRequest_even3 :: Assertion
+-- unit_handleEvalBoundedInterpRequest_even3 =
+--   let test = do
+--         expr <- gvar $ gvn ["Even3"] "even 3?"
+--         resp <-
+--           readerToState
+--             $ handleEvalBoundedInterpRequest
+--             $ EvalBoundedInterpReq
+--               { expr = expr
+--               , dir = Chk
+--               , timeout = MicroSec 10_000
+--               }
+--         expect <- con0 cFalse
+--         pure $ case resp of
+--           EvalBoundedInterpRespFailed err -> assertFailure $ show err
+--           EvalBoundedInterpRespNormal e -> e ~= expect
+--    in runAppTestM even3App test <&> fst >>= \case
+--         Left err -> assertFailure $ show err
+--         Right assertion -> assertion
+
+-- unit_handleEvalBoundedInterpRequest_mapOdd :: Assertion
+-- unit_handleEvalBoundedInterpRequest_mapOdd =
+--   let test = do
+--         expr <- gvar $ gvn ["MapOdd"] "mapOdd"
+--         resp <-
+--           readerToState
+--             $ handleEvalBoundedInterpRequest
+--             $ EvalBoundedInterpReq
+--               { expr = expr
+--               , dir = Chk
+--               , timeout = MicroSec 10_000
+--               }
+--         -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3]
+--         expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+--         pure $ case resp of
+--           EvalBoundedInterpRespFailed err -> assertFailure $ show err
+--           EvalBoundedInterpRespNormal e -> e ~= expect
+--    in runAppTestM mapOddApp test <&> fst >>= \case
+--         Left err -> assertFailure $ show err
+--         Right assertion -> assertion
+
+-- unit_handleEvalBoundedInterpRequest_mapOddPrim :: Assertion
+-- unit_handleEvalBoundedInterpRequest_mapOddPrim =
+--   let test = do
+--         expr <- gvar $ gvn ["MapOdd"] "mapOdd"
+--         resp <-
+--           readerToState
+--             $ handleEvalBoundedInterpRequest
+--             $ EvalBoundedInterpReq
+--               { expr = expr
+--               , dir = Chk
+--               , timeout = MicroSec 10_000
+--               }
+--         -- Note that the 'mapOddPrimApp' includes a program runs @mapOdd@ over a list of [0..3]
+--         expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+--         pure $ case resp of
+--           EvalBoundedInterpRespFailed err -> assertFailure $ show err
+--           EvalBoundedInterpRespNormal e -> e ~= expect
+--    in runAppTestM mapOddPrimApp test <&> fst >>= \case
+--         Left err -> assertFailure $ show err
+--         Right assertion -> assertion
+
 -- Test that 'handleEvalBoundedInterpRequest' will return timeouts.
-unit_eval_interp_handle_eval_bounded_timeout :: Assertion
-unit_eval_interp_handle_eval_bounded_timeout =
+unit_handleEvalBoundedInterpRequest_timeout :: Assertion
+unit_handleEvalBoundedInterpRequest_timeout =
   let test = do
         m' <- m
         importModules [m']
@@ -1047,8 +1201,8 @@ unit_eval_interp_handle_eval_bounded_timeout =
 
 -- Test that 'handleEvalBoundedInterpRequest' will return an error
 -- when a case branch is missing.
-unit_eval_interp_handle_eval_bounded_missing_branch :: Assertion
-unit_eval_interp_handle_eval_bounded_missing_branch =
+unit_handleEvalBoundedInterpRequest_missing_branch :: Assertion
+unit_handleEvalBoundedInterpRequest_missing_branch =
   let test = do
         m' <- m
         importModules [m']
@@ -1081,8 +1235,8 @@ unit_eval_interp_handle_eval_bounded_missing_branch =
 
 -- Test that 'handleEvalInterpRequest' will throw an 'InterpError'
 -- exception when a case branch is missing.
-unit_eval_interp_handle_eval_missing_branch :: Assertion
-unit_eval_interp_handle_eval_missing_branch =
+unit_handleEvalInterpRequest_missing_branch :: Assertion
+unit_handleEvalInterpRequest_missing_branch =
   let test = do
         m' <- m
         importModules [m']
@@ -1111,8 +1265,8 @@ unit_eval_interp_handle_eval_missing_branch =
 
 -- Test that 'handleEvalBoundedInterpRequest' will return an error
 -- when a case branch is missing (primitive version).
-unit_eval_interp_handle_eval_bounded_missing_branch_prim :: Assertion
-unit_eval_interp_handle_eval_bounded_missing_branch_prim =
+unit_handleEvalBoundedInterpRequest_missing_branch_prim :: Assertion
+unit_handleEvalBoundedInterpRequest_missing_branch_prim =
   let test = do
         m' <- m
         importModules [m']
@@ -1145,8 +1299,8 @@ unit_eval_interp_handle_eval_bounded_missing_branch_prim =
 
 -- Test that 'handleEvalInterpRequest' will throw an 'InterpError'
 -- exception when a case branch is missing (primitive version).
-unit_eval_interp_handle_eval_missing_branch_prim :: Assertion
-unit_eval_interp_handle_eval_missing_branch_prim =
+unit_handleEvalInterpRequest_missing_branch_prim :: Assertion
+unit_handleEvalInterpRequest_missing_branch_prim =
   let test = do
         m' <- m
         importModules [m']
diff --git a/primer/test/Tests/EvalFullStep.hs b/primer/test/Tests/EvalFullStep.hs
index 251a3855e..839883324 100644
--- a/primer/test/Tests/EvalFullStep.hs
+++ b/primer/test/Tests/EvalFullStep.hs
@@ -16,6 +16,8 @@ import Optics
 import Primer.App (
   EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullOptions, evalFullReqExpr),
   EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut),
+  allDefs,
+  allTypes,
   handleEvalFullRequest,
   importModules,
   newEmptyApp,
@@ -26,6 +28,7 @@ import Primer.Builtins (
   cFalse,
   cJust,
   cMakePair,
+  cNil,
   cNothing,
   cTrue,
   cZero,
@@ -46,6 +49,14 @@ import Primer.Core.Utils (
 import Primer.Def (DefMap)
 import Primer.Eval
 import Primer.EvalFullStep
+import Primer.Examples (
+  even3App,
+  even3Prog,
+  mapOddApp,
+  mapOddPrimApp,
+  mapOddPrimProg,
+  mapOddProg,
+ )
 import Primer.Gen.Core.Typed (WT, forAllT, genChk, isolateWT, propertyWT)
 import Primer.Log (runPureLogT)
 import Primer.Module (
@@ -96,6 +107,7 @@ import Primer.Test.TestM (
 import Primer.Test.Util (
   assertNoSevereLogs,
   failWhenSevereLogs,
+  gvn,
   primDefs,
   testNoSevereLogs,
   zeroIDs,
@@ -1681,9 +1693,42 @@ unit_prim_partial_map =
         s <- evalFullTestExactSteps maxID builtinTypes (gs <> prims) 91 Syn e
         s ~== r
 
+unit_evalFull_even3 :: Assertion
+unit_evalFull_even3 =
+  let (prog, maxID, _) = even3Prog
+      types = allTypes prog
+      defs = allDefs prog
+      (expr, _) = create $ gvar $ gvn ["Even3"] "even 3?"
+      (expect, _) = create $ con0 cFalse
+   in do
+        s <- evalFullTest maxID types defs 100 Chk expr
+        s <~==> Right expect
+
+unit_evalFull_mapOdd2 :: Assertion
+unit_evalFull_mapOdd2 =
+  let (prog, maxID, _) = mapOddProg 2
+      types = allTypes prog
+      defs = allDefs prog
+      (expr, _) = create $ gvar $ gvn ["MapOdd"] "mapOdd"
+      (expect, _) = create $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]
+   in do
+        s <- evalFullTest maxID types defs 200 Chk expr
+        s <~==> Right expect
+
+unit_evalFull_mapOddPrim2 :: Assertion
+unit_evalFull_mapOddPrim2 =
+  let (prog, maxID, _) = mapOddPrimProg 2
+      types = allTypes prog
+      defs = allDefs prog
+      (expr, _) = create $ gvar $ gvn ["MapOdd"] "mapOdd"
+      (expect, _) = create $ con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]
+   in do
+        s <- evalFullTest maxID types defs 200 Chk expr
+        s <~==> Right expect
+
 -- Test that handleEvalFullRequest will reduce imported terms
-unit_eval_full_modules :: Assertion
-unit_eval_full_modules =
+unit_handleEvalFullRequest_modules :: Assertion
+unit_handleEvalFullRequest_modules =
   let test = do
         builtinModule' <- builtinModule
         primitiveModule' <- primitiveModule
@@ -1708,8 +1753,8 @@ unit_eval_full_modules =
         Right assertion -> assertion
 
 -- Test that handleEvalFullRequest will reduce case analysis of imported types
-unit_eval_full_modules_scrutinize_imported_type :: Assertion
-unit_eval_full_modules_scrutinize_imported_type =
+unit_handleEvalFullRequest_modules_scrutinize_imported_type :: Assertion
+unit_handleEvalFullRequest_modules_scrutinize_imported_type =
   let test = do
         m' <- m
         importModules [m']
@@ -1744,6 +1789,71 @@ unit_eval_full_modules_scrutinize_imported_type =
           , moduleDefs = mempty
           }
 
+unit_handleEvalFullRequest_even3 :: Assertion
+unit_handleEvalFullRequest_even3 =
+  let test = do
+        expr <- gvar $ gvn ["Even3"] "even 3?"
+        resp <-
+          readerToState
+            $ handleEvalFullRequest
+            $ EvalFullReq
+              { evalFullReqExpr = expr
+              , evalFullCxtDir = Chk
+              , evalFullMaxSteps = 200
+              , evalFullOptions = UnderBinders
+              }
+        expect <- con0 cFalse
+        pure $ case resp of
+          EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out"
+          EvalFullRespNormal e -> e ~= expect
+   in runAppTestM even3App test <&> fst >>= \case
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
+unit_handleEvalFullRequest_mapOdd :: Assertion
+unit_handleEvalFullRequest_mapOdd =
+  let test = do
+        expr <- gvar $ gvn ["MapOdd"] "mapOdd"
+        resp <-
+          readerToState
+            $ handleEvalFullRequest
+            $ EvalFullReq
+              { evalFullReqExpr = expr
+              , evalFullCxtDir = Chk
+              , evalFullMaxSteps = 400
+              , evalFullOptions = UnderBinders
+              }
+        -- Note that the 'mapOddApp' includes a program runs @mapOdd@ over a list of [0..3]
+        expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+        pure $ case resp of
+          EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out"
+          EvalFullRespNormal e -> e ~= expect
+   in runAppTestM mapOddApp test <&> fst >>= \case
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
+unit_handleEvalFullRequest_mapOddPrim :: Assertion
+unit_handleEvalFullRequest_mapOddPrim =
+  let test = do
+        expr <- gvar $ gvn ["MapOdd"] "mapOdd"
+        resp <-
+          readerToState
+            $ handleEvalFullRequest
+            $ EvalFullReq
+              { evalFullReqExpr = expr
+              , evalFullCxtDir = Chk
+              , evalFullMaxSteps = 300
+              , evalFullOptions = UnderBinders
+              }
+        -- Note that the 'mapOddPrimApp' includes a program runs @mapOddPrim@ over a list of [0..3]
+        expect <- con cCons [con0 cFalse, con cCons [con0 cTrue, con cCons [con0 cFalse, con cCons [con0 cTrue, con cNil []]]]]
+        pure $ case resp of
+          EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out"
+          EvalFullRespNormal e -> e ~= expect
+   in runAppTestM mapOddPrimApp test <&> fst >>= \case
+        Left err -> assertFailure $ show err
+        Right assertion -> assertion
+
 -- Test that evaluation does not duplicate node IDs
 tasty_unique_ids :: Property
 tasty_unique_ids = withTests 1000