diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs
index 46cf5d4ed..3c532e8dd 100644
--- a/primer-api/src/Primer/API.hs
+++ b/primer-api/src/Primer/API.hs
@@ -216,6 +216,7 @@ import Primer.Def (
   defAST,
  )
 import Primer.Def qualified as Def
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.Eval.Redex (Dir (Chk), EvalLog)
 import Primer.EvalFull (TerminationBound)
 import Primer.JSON (
@@ -1128,6 +1129,7 @@ evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
             { evalFullReqExpr = e
             , evalFullCxtDir = Chk
             , evalFullMaxSteps = fromMaybe 10 lim
+            , evalFullOptions = UnderBinders -- TODO/REVIEW: should we expose this to the actual api? If so, the BREAKING CHANGE commit message needs updating
             }
       pure $ case x of
         App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e'
diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs
index 9ec3168c3..e9f5bec9d 100644
--- a/primer-benchmark/src/Benchmarks.hs
+++ b/primer-benchmark/src/Benchmarks.hs
@@ -20,6 +20,7 @@ import Primer.App (
   tcWholeProgWithImports,
  )
 import Primer.App.Utils (forgetProgTypecache)
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.EvalFull (
   Dir (Syn),
   EvalLog,
@@ -101,11 +102,11 @@ benchmarks =
     evalTestMPureLogs e maxEvals =
       evalTestM (maxID e) $
         runPureLogT $
-          evalFull @EvalLog builtinTypes (defMap e) maxEvals Syn (expr e)
+          evalFull @EvalLog UnderBinders builtinTypes (defMap e) maxEvals Syn (expr e)
     evalTestMDiscardLogs e maxEvals =
       evalTestM (maxID e) $
         runDiscardLogT $
-          evalFull @EvalLog builtinTypes (defMap e) maxEvals Syn (expr e)
+          evalFull @EvalLog UnderBinders builtinTypes (defMap e) maxEvals Syn (expr e)
 
     benchExpected f g e n b = EnvBench e n $ \e' ->
       NF
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 53def917e..b476b92b0 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -466,6 +466,7 @@ data MutationRequest
 data EvalReq = EvalReq
   { evalReqExpr :: Expr
   , evalReqRedex :: ID
+  , evalReqOptions :: Eval.NormalOrderOptions
   }
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON EvalReq
@@ -482,6 +483,7 @@ data EvalFullReq = EvalFullReq
   { evalFullReqExpr :: Expr
   , evalFullCxtDir :: Dir -- is this expression in a syn/chk context, so we can tell if is an embedding.
   , evalFullMaxSteps :: TerminationBound
+  , evalFullOptions :: Eval.NormalOrderOptions
   }
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON EvalFullReq
@@ -577,7 +579,7 @@ handleEvalRequest req = do
   case result of
     Left err -> throwError' err
     Right (expr, detail) -> do
-      redexes <- Eval.redexes (allTypes prog) (allDefs prog) Syn expr
+      redexes <- Eval.redexes (evalReqOptions req) (allTypes prog) (allDefs prog) Syn expr
       pure
         EvalResp
           { evalRespExpr = expr
@@ -590,10 +592,10 @@ handleEvalFullRequest ::
   (MonadQueryApp m e, MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
   EvalFullReq ->
   m EvalFullResp
-handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps}) = do
+handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps, evalFullOptions}) = do
   app <- ask
   let prog = appProg app
-  result <- runFreshM app $ evalFull (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  result <- runFreshM app $ evalFull evalFullOptions (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
   pure $ case result of
     Left (TimedOut e) -> EvalFullRespTimedOut e
     Right nf -> EvalFullRespNormal nf
diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs
index 40ae50a28..8b78db6b2 100644
--- a/primer/src/Primer/Eval.hs
+++ b/primer/src/Primer/Eval.hs
@@ -5,6 +5,7 @@ module Primer.Eval (
   -- The public API of this module
   step,
   redexes,
+  NormalOrderOptions (..),
   EvalLog (..),
   EvalError (..),
   EvalDetail (..),
@@ -53,6 +54,7 @@ import Primer.Eval.Detail (
 import Primer.Eval.EvalError (EvalError (..))
 import Primer.Eval.NormalOrder (
   FMExpr (FMExpr, expr, subst, substTy, ty),
+  NormalOrderOptions (..),
   foldMapExpr,
   singletonCxt,
  )
@@ -108,6 +110,7 @@ step tydefs globals expr d i = runExceptT $ do
 findNodeByID :: ID -> Dir -> Expr -> Maybe (Cxt, Either (Dir, ExprZ) TypeZ)
 findNodeByID i =
   foldMapExpr
+    UnderBinders
     FMExpr
       { expr = \ez d c -> if getID ez == i then Just (c, Left (d, ez)) else Nothing
       , ty = \tz c -> if getID tz == i then Just (c, Right tz) else Nothing
@@ -122,14 +125,16 @@ findNodeByID i =
 redexes ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  NormalOrderOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   m [ID]
-redexes tydefs globals =
+redexes opts tydefs globals =
   (ListT.toList .)
     . foldMapExpr
+      opts
       FMExpr
         { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex tydefs globals d (target ez))
         , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType (target tz))
diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
index 0a196e99b..73508b5c0 100644
--- a/primer/src/Primer/Eval/NormalOrder.hs
+++ b/primer/src/Primer/Eval/NormalOrder.hs
@@ -7,6 +7,7 @@ module Primer.Eval.NormalOrder (
   findRedex,
   foldMapExpr,
   FMExpr (..),
+  NormalOrderOptions (..),
   -- Exported for testing
   singletonCxt,
 ) where
@@ -95,6 +96,7 @@ import Primer.Eval.Redex (
   viewRedexType,
   _freeVarsLetBinding,
  )
+import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.Log (ConvertLogMessage)
 import Primer.Name (Name)
 import Primer.TypeDef (
@@ -129,12 +131,17 @@ data RedexWithContext
   | RType TypeZ RedexType
 
 viewLet :: (Dir, ExprZ) -> Maybe (LetBinding, Accum Cxt (Dir, ExprZ))
-viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
+viewLet dez@(_, ez) = case (target ez, exprChildren' dez) of
   (Let _ x e _b, [_, bz]) -> Just (LetBind x e, bz)
   (Letrec _ x e ty _b, [_, bz]) -> Just (LetrecBind x e ty, bz)
   (LetType _ a ty _b, [bz]) -> bz `seq` Just (LetTyBind $ LetTypeBind a ty, bz)
   _ -> Nothing
 
+data NormalOrderOptions -- TODO/REVIEW: this is a bit of a misnomer, as it affects `Eval.redexes`, which is only used for single-step. NB: even if we set StopAtBinders, we can still call `Eval.step` with the id of a redex under a binder and it will reduce, even though `redexes` will not report that id
+  = UnderBinders
+  deriving stock (Eq, Show, Read, Generic)
+  deriving (FromJSON, ToJSON) via PrimerJSON NormalOrderOptions
+
 -- | This is similar to 'foldMap', with a few differences:
 -- - 'Expr' is not foldable
 -- - We target every subexpression and also every (nested) subtype (e.g. in an annotation)
@@ -151,8 +158,13 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
 -- However, we may reduce type children to normal form more eagerly than necessary,
 -- both reducing type annotations more than needed, and reducing type applications when not needed.
 -- Since computation in types is strongly normalising, this will not cause us to fail to find any normal forms.
-foldMapExpr :: forall f a. MonadPlus f => FMExpr (f a) -> Dir -> Expr -> f a
-foldMapExpr extract topDir = flip evalAccumT mempty . go . (topDir,) . focus
+--
+-- We can optionally stop when we find a binder (e.g. to implement closed
+-- evaluation -- do not compute under binders), although for consistency we
+-- treat all case branches as being binders, even those that do not actually
+-- bind a variable.
+foldMapExpr :: forall f a. MonadPlus f => NormalOrderOptions -> FMExpr (f a) -> Dir -> Expr -> f a
+foldMapExpr opts extract topDir = flip evalAccumT mempty . go . (topDir,) . focus
   where
     go :: (Dir, ExprZ) -> AccumT Cxt f a
     go dez@(d, ez) =
@@ -164,7 +176,7 @@ foldMapExpr extract topDir = flip evalAccumT mempty . go . (topDir,) . focus
           _ ->
             msum $
               (goType =<< focusType' ez)
-                : map (go <=< hoistAccum) (exprChildren dez)
+                : map (go <=< hoistAccum) (exprChildren opts dez)
     goType :: TypeZ -> AccumT Cxt f a
     goType tz =
       readerToAccumT (ReaderT $ extract.ty tz)
@@ -205,13 +217,15 @@ hoistAccum = Foreword.hoistAccum generalize
 findRedex ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  NormalOrderOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   MaybeT m RedexWithContext
-findRedex tydefs globals =
+findRedex opts tydefs globals =
   foldMapExpr
+    opts
     ( FMExpr
         { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex tydefs globals d (target ez))
         , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType (target tz))
@@ -255,7 +269,8 @@ findRedex tydefs globals =
                   _ -> mzero
              in msum @[] $
                   Foreword.hoistAccum hoistMaybe (substTyChild =<< focusType' ez)
-                    : map (substChild <=< hoistAccum) (exprChildren (d, ez))
+                    -- Note that we need to go under binders when substituting
+                    : map (substChild <=< hoistAccum) (exprChildren' (d, ez))
        in here <|> innerLet <|> dive
     goSubstTy :: TyVarName -> Type -> TypeZ -> AccumT Cxt Maybe RedexWithContext
     goSubstTy v t tz =
@@ -291,8 +306,10 @@ children' z = case down z of
   Nothing -> mempty
   Just z' -> z' : unfoldr (fmap (\x -> (x, x)) . right) z'
 
-exprChildren :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
-exprChildren (d, ez) =
+-- All children of the current focus, monadically adding any bindings of which
+-- we have just entered the scope.
+exprChildren' :: (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
+exprChildren' (d, ez) =
   children' ez <&> \c -> do
     let bs = getBoundHere' (target ez) (Just $ target c)
     let d' = case target ez of
@@ -313,6 +330,10 @@ exprChildren (d, ez) =
     addBinds ez bs
     pure (d', c)
 
+exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [Accum Cxt (Dir, ExprZ)]
+exprChildren = \case
+  UnderBinders -> exprChildren'
+
 typeChildren :: TypeZ -> [Accum Cxt TypeZ]
 typeChildren tz =
   children' tz <&> \c -> do
diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFull.hs
index 8dca22531..80168439f 100644
--- a/primer/src/Primer/EvalFull.hs
+++ b/primer/src/Primer/EvalFull.hs
@@ -22,7 +22,7 @@ import Primer.Core (
 import Primer.Def (
   DefMap,
  )
-import Primer.Eval.NormalOrder (RedexWithContext (RExpr, RType), findRedex)
+import Primer.Eval.NormalOrder (NormalOrderOptions, RedexWithContext (RExpr, RType), findRedex)
 import Primer.Eval.Redex (
   Dir (Chk, Syn),
   EvalLog (..),
@@ -49,8 +49,16 @@ newtype EvalFullError
 type TerminationBound = Natural
 
 -- A naive implementation of normal-order reduction
-evalFull :: MonadEval l m => TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
-evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr
+evalFull ::
+  MonadEval l m =>
+  NormalOrderOptions ->
+  TypeDefMap ->
+  DefMap ->
+  TerminationBound ->
+  Dir ->
+  Expr ->
+  m (Either EvalFullError Expr)
+evalFull opts tydefs env n d expr = snd <$> evalFullStepCount opts tydefs env n d expr
 
 -- | As 'evalFull', but also returns how many reduction steps were taken.
 -- (This is mostly useful for testing purposes.)
@@ -62,26 +70,27 @@ evalFull tydefs env n d expr = snd <$> evalFullStepCount tydefs env n d expr
 -- more to notice termination.
 evalFullStepCount ::
   MonadEval l m =>
+  NormalOrderOptions ->
   TypeDefMap ->
   DefMap ->
   TerminationBound ->
   Dir ->
   Expr ->
   m (Natural, Either EvalFullError Expr)
-evalFullStepCount tydefs env n d = go 0
+evalFullStepCount opts tydefs env n d = go 0
   where
     go s expr
       | s >= n = pure (s, Left $ TimedOut expr)
       | otherwise =
-          runMaybeT (step tydefs env d expr) >>= \case
+          runMaybeT (step opts tydefs env d expr) >>= \case
             Nothing -> pure (s, Right expr) -- this is a normal form
             Just e -> go (s + 1) e
 
 -- The 'Dir' argument only affects what happens if the root is an annotation:
 -- do we keep it (Syn) or remove it (Chk). I.e. is an upsilon reduction allowed
 -- at the root?
-step :: MonadEval l m => TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
-step tydefs g d e =
-  findRedex tydefs g d e >>= \case
+step :: MonadEval l m => NormalOrderOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
+step opts tydefs g d e =
+  findRedex opts tydefs g d e >>= \case
     RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex r
     RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy r
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index 5cc15abae..a80b3b782 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -12,7 +12,7 @@ import Hedgehog (annotateShow, assert, discard, failure, label, success, (===))
 import Hedgehog.Gen qualified as Gen
 import Optics (elemOf, (^.))
 import Primer.App (
-  EvalReq (EvalReq, evalReqExpr, evalReqRedex),
+  EvalReq (EvalReq, evalReqExpr, evalReqOptions, evalReqRedex),
   EvalResp (EvalResp, evalRespExpr),
   handleEvalRequest,
   importModules,
@@ -58,6 +58,7 @@ import Primer.Eval (
   GlobalVarInlineDetail (..),
   LetRemovalDetail (..),
   LocalVarInlineDetail (..),
+  NormalOrderOptions (UnderBinders),
   findNodeByID,
   getNonCapturedLocal,
   redexes,
@@ -985,7 +986,7 @@ unit_findNodeByID_capture_type =
 -- | A helper for these tests
 redexes' :: TypeDefMap -> DefMap -> Dir -> Expr -> IO (Set ID)
 redexes' types prims d e = do
-  let (rs, logs) = runPureLog $ redexes types prims d e
+  let (rs, logs) = runPureLog $ redexes UnderBinders types prims d e
   assertNoSevereLogs @EvalLog logs
   pure $ Set.fromList rs
 
@@ -1379,7 +1380,7 @@ unit_eval_modules =
         EvalResp{evalRespExpr = e} <-
           readerToState $
             handleEvalRequest
-              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo}
+              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo, evalReqOptions = UnderBinders}
         expect <- char 'A'
         pure $ e ~= expect
       a = newEmptyApp
@@ -1400,7 +1401,7 @@ unit_eval_modules_scrutinize_imported_type =
         EvalResp{evalRespExpr = e} <-
           readerToState $
             handleEvalRequest
-              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo}
+              EvalReq{evalReqExpr = foo, evalReqRedex = getID foo, evalReqOptions = UnderBinders}
         expect <- con0 cFalse
         pure $ e ~= expect
       a = newEmptyApp
@@ -1429,7 +1430,8 @@ tasty_type_preservation =
             let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
             tds <- asks typeDefs
             (dir, t, ty) <- genDirTm
-            rs <- failWhenSevereLogs $ redexes @EvalLog tds globs dir t
+            closed <- forAllT $ Gen.element [UnderBinders]
+            rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t
             when (null rs) discard
             r <- forAllT $ Gen.element rs
             s <- failWhenSevereLogs $ step @EvalLog tds globs t dir r
@@ -1457,7 +1459,8 @@ tasty_redex_independent =
             (dir, t, _) <- genDirTm
             annotateShow dir
             annotateShow t
-            rs <- failWhenSevereLogs $ redexes @EvalLog tds globs dir t
+            closed <- forAllT $ Gen.element [UnderBinders]
+            rs <- failWhenSevereLogs $ redexes @EvalLog closed tds globs dir t
             when (length rs <= 1) discard
             i <- forAllT $ Gen.element rs
             j <- forAllT $ Gen.element $ delete i rs
@@ -1471,5 +1474,5 @@ tasty_redex_independent =
                     sj <- failWhenSevereLogs $ step @EvalLog tds globs t dir j
                     case sj of
                       Right (_, BindRename{}) -> success
-                      _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog tds globs dir s')
+                      _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog closed tds globs dir s')
                   else success
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index 8d2eab520..11e958dfd 100644
--- a/primer/test/Tests/EvalFull.hs
+++ b/primer/test/Tests/EvalFull.hs
@@ -14,7 +14,7 @@ import Hedgehog.Internal.Property (LabelName (unLabelName))
 import Hedgehog.Range qualified as Range
 import Optics
 import Primer.App (
-  EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullReqExpr),
+  EvalFullReq (EvalFullReq, evalFullCxtDir, evalFullMaxSteps, evalFullOptions, evalFullReqExpr),
   EvalFullResp (EvalFullRespNormal, EvalFullRespTimedOut),
   handleEvalFullRequest,
   importModules,
@@ -43,6 +43,7 @@ import Primer.Core.Utils (
   forgetMetadata,
  )
 import Primer.Def (DefMap)
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.EvalFull
 import Primer.Examples qualified as Examples (
   even,
@@ -446,6 +447,7 @@ resumeTest mods dir t = do
   let globs = foldMap' moduleDefsQualified mods
   tds <- asks typeDefs
   n <- forAllT $ Gen.integral $ Range.linear 2 1000 -- Arbitrary limit here
+  closed <- forAllT $ Gen.element [UnderBinders]
   -- NB: We need to run this first reduction in an isolated context
   -- as we need to avoid it changing the fresh-name-generator state
   -- for the next run (sMid and sTotal). This is because reduction may need
@@ -453,19 +455,19 @@ resumeTest mods dir t = do
   -- exactly the same as "reducing n steps and then further reducing m
   -- steps" (including generated names). (A happy consequence of this is that
   -- it is precisely the same including ids in metadata.)
-  ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog tds globs n dir t
+  ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog closed tds globs n dir t
   testNoSevereLogs logs
   when (stepsFinal' < 2) discard
   let stepsFinal = case sFinal of Left _ -> stepsFinal'; Right _ -> 1 + stepsFinal'
   m <- forAllT $ Gen.integral $ Range.constant 1 (stepsFinal - 1)
-  (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs m dir t
+  (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed tds globs m dir t
   stepsMid === m
   sMid <- case sMid' of
     Left (TimedOut e) -> pure e
     -- This should never happen: we know we are not taking enough steps to
     -- hit a normal form (as m < stepsFinal)
     Right e -> assert False >> pure e
-  (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs (stepsFinal - m) dir sMid
+  (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed tds globs (stepsFinal - m) dir sMid
   stepsMid + stepsTotal === stepsFinal'
   sFinal === sTotal
 
@@ -820,7 +822,8 @@ tasty_type_preservation = withTests 1000 $
                 s' <- checkTest ty s
                 forgetMetadata s === forgetMetadata s' -- check no smart holes happened
       maxSteps <- forAllT $ Gen.integral $ Range.linear 1 1000 -- Arbitrary limit here
-      (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs maxSteps dir t
+      closed <- forAllT $ Gen.element [UnderBinders]
+      (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed tds globs maxSteps dir t
       annotateShow steps
       annotateShow s
       -- s is often reduced to normal form
@@ -830,7 +833,7 @@ tasty_type_preservation = withTests 1000 $
         then label "generated a normal form"
         else do
           midSteps <- forAllT $ Gen.integral $ Range.linear 1 (steps - 1)
-          (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog tds globs midSteps dir t
+          (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed tds globs midSteps dir t
           test "mid " s'
 
 -- Unsaturated primitives are stuck terms
@@ -1281,6 +1284,7 @@ unit_eval_full_modules =
                 { evalFullReqExpr = foo
                 , evalFullCxtDir = Chk
                 , evalFullMaxSteps = 2
+                , evalFullOptions = UnderBinders
                 }
         expect <- char 'A'
         pure $ case resp of
@@ -1303,8 +1307,13 @@ unit_eval_full_modules_scrutinize_imported_type =
             [branch cTrue [] $ con0 cFalse, branch cFalse [] $ con0 cTrue]
         resp <-
           readerToState $
-            handleEvalFullRequest
-              EvalFullReq{evalFullReqExpr = foo, evalFullCxtDir = Chk, evalFullMaxSteps = 2}
+            handleEvalFullRequest $
+              EvalFullReq
+                { evalFullReqExpr = foo
+                , evalFullCxtDir = Chk
+                , evalFullMaxSteps = 2
+                , evalFullOptions = UnderBinders
+                }
         expect <- con0 cFalse
         pure $ case resp of
           EvalFullRespTimedOut _ -> assertFailure "EvalFull timed out"
@@ -1331,10 +1340,11 @@ tasty_unique_ids = withTests 1000 $
       let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
       tds <- asks typeDefs
       (dir, t1, _) <- genDirTm
+      closed <- forAllT $ Gen.element [UnderBinders]
       let go n t
             | n == (0 :: Int) = pure ()
             | otherwise = do
-                t' <- failWhenSevereLogs $ evalFull @EvalLog tds globs 1 dir t
+                t' <- failWhenSevereLogs $ evalFull @EvalLog closed tds globs 1 dir t
                 case t' of
                   Left (TimedOut e) -> uniqueIDs e >> go (n - 1) e
                   Right e -> uniqueIDs e
@@ -1403,14 +1413,14 @@ unit_case_prim =
 
 evalFullTest :: ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
 evalFullTest id_ tydefs globals n d e = do
-  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog tydefs globals n d e
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog UnderBinders tydefs globals n d e
   assertNoSevereLogs logs
   distinctIDs r
   pure r
 
 evalFullTasty :: MonadTest m => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
 evalFullTasty id_ tydefs globals n d e = do
-  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog tydefs globals n d e
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog UnderBinders tydefs globals n d e
   testNoSevereLogs logs
   let ids = r ^.. evalResultExpr % exprIDs
   ids === ordNub ids
diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs
index c37c95685..a7f5e3f29 100644
--- a/primer/test/Tests/Prelude/Utils.hs
+++ b/primer/test/Tests/Prelude/Utils.hs
@@ -7,6 +7,7 @@ import Hedgehog.Internal.Property
 import Optics (over)
 import Primer.Core (Expr, GVarName, Type)
 import Primer.Core.DSL (apps', create', gvar)
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.EvalFull (Dir (Chk), EvalFullError, EvalLog, TerminationBound, evalFull)
 import Primer.Log (runPureLogT)
 import Primer.Module (builtinModule, moduleDefsQualified, moduleTypesQualified, primitiveModule)
@@ -51,7 +52,7 @@ functionOutput' :: GVarName -> [Either (TestM Expr) (TestM Type)] -> Termination
 functionOutput' f args depth =
   let (r, logs) = evalTestM 0 $ runPureLogT $ do
         e <- apps' (gvar f) $ bimap lift lift <$> args
-        evalFull @EvalLog ty def n d e
+        evalFull @EvalLog UnderBinders ty def n d e
       severe = Seq.filter isSevereLog logs
    in if null severe
         then r
diff --git a/primer/test/Tests/Undo.hs b/primer/test/Tests/Undo.hs
index 1b45cad97..598fad856 100644
--- a/primer/test/Tests/Undo.hs
+++ b/primer/test/Tests/Undo.hs
@@ -24,7 +24,7 @@ import Primer.Core (
   qualifyName,
  )
 import Primer.Def (astDefExpr, defAST)
-import Primer.Eval (Dir (Syn))
+import Primer.Eval (Dir (Syn), NormalOrderOptions (UnderBinders))
 import Primer.Module (
   moduleDefsQualified,
   moduleName,
@@ -73,6 +73,7 @@ unit_redo_eval =
               { App.evalFullReqExpr = Var (Meta 0 Nothing Nothing) (GlobalVarRef $ qualifyName scope "main")
               , App.evalFullCxtDir = Syn
               , App.evalFullMaxSteps = 10
+              , App.evalFullOptions = UnderBinders
               }
       edit1 = handleEditRequest action1
       edit2 = handleEditRequest . action2