diff --git a/primer-api/src/Primer/API.hs b/primer-api/src/Primer/API.hs
index 7d0b2f544..2f8055d2e 100644
--- a/primer-api/src/Primer/API.hs
+++ b/primer-api/src/Primer/API.hs
@@ -226,6 +226,7 @@ import Primer.Def (
   defAST,
  )
 import Primer.Def qualified as Def
+import Primer.Eval (NormalOrderOptions (StopAtBinders))
 import Primer.Eval.Redex (Dir (Chk), EvalLog)
 import Primer.EvalFull (TerminationBound)
 import Primer.JSON (
@@ -412,7 +413,7 @@ data APILog
   | GenerateNames (ReqResp (SessionId, ((GVarName, ID), Either (Maybe (Type' ())) (Maybe (Kind' ())))) (Either ProgError [Name.Name]))
   | EvalStep (ReqResp (SessionId, EvalReq) (Either ProgError EvalResp))
   | EvalFull (ReqResp (SessionId, EvalFullReq) (Either ProgError App.EvalFullResp))
-  | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, GVarName) EvalFullResp)
+  | EvalFull' (ReqResp (SessionId, Maybe TerminationBound, Maybe NormalOrderOptions, GVarName) EvalFullResp)
   | FlushSessions (ReqResp () ())
   | CreateDef (ReqResp (SessionId, ModuleName, Maybe Text) Prog)
   | CreateTypeDef (ReqResp (SessionId, TyConName, [ValConName]) Prog)
@@ -1117,16 +1118,18 @@ evalFull' ::
   (MonadIO m, MonadThrow m, MonadAPILog l m, ConvertLogMessage EvalLog l) =>
   SessionId ->
   Maybe TerminationBound ->
+  Maybe NormalOrderOptions ->
   GVarName ->
   PrimerM m EvalFullResp
-evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
-  noErr <$> liftQueryAppM (q lim d) sid
+evalFull' = curry4 $ logAPI (noError EvalFull') $ \(sid, lim, closed, d) ->
+  noErr <$> liftQueryAppM (q lim closed d) sid
   where
     q ::
       Maybe TerminationBound ->
+      Maybe NormalOrderOptions ->
       GVarName ->
       QueryAppM (PureLog (WithSeverity l)) Void EvalFullResp
-    q lim d = do
+    q lim closed d = do
       -- We don't care about uniqueness of this ID, and we do not want to
       -- disturb any FreshID state, since that could break undo/redo.
       -- The reason we don't care about uniqueness is that this node will never
@@ -1139,6 +1142,7 @@ evalFull' = curry3 $ logAPI (noError EvalFull') $ \(sid, lim, d) ->
             { evalFullReqExpr = e
             , evalFullCxtDir = Chk
             , evalFullMaxSteps = fromMaybe 10 lim
+            , evalFullOptions = fromMaybe StopAtBinders closed
             }
       pure $ case x of
         App.EvalFullRespTimedOut e' -> EvalFullRespTimedOut $ viewTreeExpr e'
diff --git a/primer-api/test/Tests/API.hs b/primer-api/test/Tests/API.hs
index 354f2a20a..6d178081a 100644
--- a/primer-api/test/Tests/API.hs
+++ b/primer-api/test/Tests/API.hs
@@ -48,6 +48,7 @@ import Primer.Database (
   fromSessionName,
  )
 import Primer.Def (astDefExpr, astDefType, defAST)
+import Primer.Eval (NormalOrderOptions (UnderBinders))
 import Primer.Examples (
   comprehensive,
   even3App,
@@ -462,7 +463,7 @@ test_eval_undo =
       sid <- newSession $ NewSessionReq "a new session" True
       let scope = mkSimpleModuleName "Main"
       step "eval"
-      void $ evalFull' sid (Just 100) $ qualifyName scope "main"
+      void $ evalFull' sid (Just 100) (Just UnderBinders) $ qualifyName scope "main"
       step "insert λ"
       let getMain = do
             p <- getProgram sid
diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs
index d0b6100e0..e985342b3 100644
--- a/primer-benchmark/src/Benchmarks.hs
+++ b/primer-benchmark/src/Benchmarks.hs
@@ -21,6 +21,7 @@ import Primer.App (
  )
 import Primer.App.Utils (forgetProgTypecache)
 import Primer.Eval (
+  NormalOrderOptions (UnderBinders),
   RunRedexOptions (RunRedexOptions, pushAndElide),
   ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets),
  )
@@ -102,16 +103,17 @@ benchmarks =
       ]
   ]
   where
+    evalOptionsN = UnderBinders
     evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
     evalOptionsR = RunRedexOptions{pushAndElide = True}
     evalTestMPureLogs e maxEvals =
       evalTestM (maxID e) $
         runPureLogT $
-          evalFull @EvalLog evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e)
+          evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e)
     evalTestMDiscardLogs e maxEvals =
       evalTestM (maxID e) $
         runDiscardLogT $
-          evalFull @EvalLog evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e)
+          evalFull @EvalLog evalOptionsN evalOptionsV evalOptionsR builtinTypes (defMap e) maxEvals Syn (expr e)
 
     benchExpected f g e n b = EnvBench e n $ \e' ->
       NF
diff --git a/primer-service/src/Primer/OpenAPI.hs b/primer-service/src/Primer/OpenAPI.hs
index 75ec584e1..9717c7723 100644
--- a/primer-service/src/Primer/OpenAPI.hs
+++ b/primer-service/src/Primer/OpenAPI.hs
@@ -82,6 +82,7 @@ import Primer.Database (
   Session,
   SessionName,
  )
+import Primer.Eval (NormalOrderOptions)
 import Primer.JSON (CustomJSON (CustomJSON), PrimerJSON)
 import Primer.Name (Name)
 import Servant.API (FromHttpApiData (parseQueryParam), ToHttpApiData (toQueryParam))
@@ -198,6 +199,11 @@ instance FromHttpApiData Level where
   parseQueryParam = parseQueryParamRead "level"
 instance ToHttpApiData Level where
   toQueryParam = show
+deriving anyclass instance ToParamSchema NormalOrderOptions
+instance FromHttpApiData NormalOrderOptions where
+  parseQueryParam = parseQueryParamRead "NormalOrderOptions"
+instance ToHttpApiData NormalOrderOptions where
+  toQueryParam = show
 parseQueryParamRead :: Read a => Text -> Text -> Either Text a
 parseQueryParamRead m t = maybeToEither ("unknown " <> m <> ": " <> t) $ readMaybe t
 
diff --git a/primer-service/src/Primer/Servant/OpenAPI.hs b/primer-service/src/Primer/Servant/OpenAPI.hs
index 0e69348cd..e75b4b9b2 100644
--- a/primer-service/src/Primer/Servant/OpenAPI.hs
+++ b/primer-service/src/Primer/Servant/OpenAPI.hs
@@ -23,6 +23,7 @@ import Primer.Core (GVarName, ModuleName)
 import Primer.Database (
   SessionId,
  )
+import Primer.Eval (NormalOrderOptions)
 import Primer.Finite (Finite)
 import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.OpenAPI ()
@@ -124,6 +125,7 @@ data SessionAPI mode = SessionAPI
           :> Summary "Evaluate the named definition to normal form (or time out)"
           :> OperationId "eval-full"
           :> QueryParam "stepLimit" (Finite 0 EvalFullStepLimit)
+          :> QueryParam "closed" NormalOrderOptions
           :> ReqBody '[JSON] GVarName
           :> Post '[JSON] EvalFullResp
   , undo ::
diff --git a/primer-service/test/outputs/OpenAPI/openapi.json b/primer-service/test/outputs/OpenAPI/openapi.json
index bfa6bc197..b852a7a8c 100644
--- a/primer-service/test/outputs/OpenAPI/openapi.json
+++ b/primer-service/test/outputs/OpenAPI/openapi.json
@@ -1486,6 +1486,18 @@
                             "minimum": 0,
                             "type": "integer"
                         }
+                    },
+                    {
+                        "in": "query",
+                        "name": "closed",
+                        "required": false,
+                        "schema": {
+                            "enum": [
+                                "UnderBinders",
+                                "StopAtBinders"
+                            ],
+                            "type": "string"
+                        }
                     }
                 ],
                 "requestBody": {
@@ -1509,7 +1521,7 @@
                         "description": ""
                     },
                     "400": {
-                        "description": "Invalid `body` or `stepLimit`"
+                        "description": "Invalid `body` or `closed` or `stepLimit`"
                     },
                     "404": {
                         "description": "`sessionId` not found"
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index a852bad85..8715376bf 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -487,6 +487,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
@@ -595,12 +596,12 @@ 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
   let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
   let optsR = RunRedexOptions{pushAndElide = True}
-  result <- runFreshM app $ evalFull optsV optsR (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
+  result <- runFreshM app $ evalFull evalFullOptions optsV optsR (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 23b0409c7..cc8612db5 100644
--- a/primer/src/Primer/Eval.hs
+++ b/primer/src/Primer/Eval.hs
@@ -7,6 +7,7 @@ module Primer.Eval (
   redexes,
   RunRedexOptions (..),
   ViewRedexOptions (..),
+  NormalOrderOptions (..),
   EvalLog (..),
   EvalError (..),
   EvalDetail (..),
@@ -57,6 +58,7 @@ import Primer.Eval.Detail (
 import Primer.Eval.EvalError (EvalError (..))
 import Primer.Eval.NormalOrder (
   FMExpr (FMExpr, expr, ty),
+  NormalOrderOptions (..),
   foldMapExpr,
   singletonCxt,
  )
@@ -114,6 +116,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
@@ -132,6 +135,11 @@ evalOpts =
 -- We assume that the expression is well scoped. There are no
 -- guarantees about whether we will claim that an ill-sorted variable
 -- is inlinable, e.g. @lettype a = _ in case a of ...@.
+--
+-- NB: we return /all/ redexes, even those under binders. We ignore any
+-- `NormalOrderOptions`. This means that more redexes may be returned than an
+-- EvalFull would actually reduce (depending on the NormalOrderOptions given to
+-- EvalFull).
 redexes ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
@@ -143,6 +151,7 @@ redexes ::
 redexes tydefs globals =
   (ListT.toList .)
     . foldMapExpr
+      UnderBinders
       FMExpr
         { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex evalOpts tydefs globals d (target ez))
         , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType evalOpts (target tz))
diff --git a/primer/src/Primer/Eval/NormalOrder.hs b/primer/src/Primer/Eval/NormalOrder.hs
index 1291fdb5d..7db17bbff 100644
--- a/primer/src/Primer/Eval/NormalOrder.hs
+++ b/primer/src/Primer/Eval/NormalOrder.hs
@@ -6,6 +6,7 @@ module Primer.Eval.NormalOrder (
   findRedex,
   foldMapExpr,
   FMExpr (..),
+  NormalOrderOptions (..),
   -- Exported for testing
   singletonCxt,
 ) where
@@ -21,11 +22,14 @@ import Primer.Core (
     App,
     Case,
     Hole,
+    LAM,
+    Lam,
     Let,
     LetType,
     Letrec
   ),
   Type' (
+    TForall,
     TLet
   ),
  )
@@ -43,6 +47,7 @@ import Primer.Eval.Redex (
   viewRedex,
   viewRedexType,
  )
+import Primer.JSON (CustomJSON (CustomJSON), FromJSON, PrimerJSON, ToJSON)
 import Primer.Log (ConvertLogMessage)
 import Primer.TypeDef (
   TypeDefMap,
@@ -81,7 +86,7 @@ data ViewLet = ViewLet
   -- ^ any non-body term children (i.e. rhs of the binding)
   }
 viewLet :: (Dir, ExprZ) -> Maybe ViewLet
-viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
+viewLet dez@(_, ez) = case (target ez, exprChildren UnderBinders dez) of
   (Let _ x e _b, [ez', bz]) -> Just (ViewLet (LetBind x e) bz [] [ez'])
   (Letrec _ x e ty _b, [ez', bz]) -> Just (ViewLet (LetrecBind x e ty) bz tz [ez'])
   (LetType _ a ty _b, [bz]) -> bz `seq` Just (ViewLet (LetTyBind $ LetTypeBind a ty) bz tz [])
@@ -90,6 +95,12 @@ viewLet dez@(_, ez) = case (target ez, exprChildren dez) of
     tz :: [TypeZ]
     tz = maybeToList $ focusType ez
 
+data NormalOrderOptions
+  = UnderBinders
+  | StopAtBinders
+  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)
@@ -107,8 +118,15 @@ 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 = go mempty . (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. Note that (for the case where we reduce a stack of @let@s
+-- one-by-one inside-out) we need to go under let bindings, but stop when we
+-- find a non-@let@.
+foldMapExpr :: forall f a. MonadPlus f => NormalOrderOptions -> FMExpr (f a) -> Dir -> Expr -> f a
+foldMapExpr opts extract topDir = go mempty . (topDir,) . focus
   where
     go :: Cxt -> (Dir, ExprZ) -> f a
     go lets dez@(d, ez) =
@@ -125,17 +143,20 @@ foldMapExpr extract topDir = go mempty . (topDir,) . focus
           -- its type annotation, we can handle them all uniformly
           -- Since this node is not a let, the context is reset
           _ ->
-            msum $
-              (goType mempty =<< focusType' ez)
-                : map (go mempty) (exprChildren dez)
+            case (opts, lets) of
+              (StopAtBinders, Cxt (_ : _)) -> mzero
+              _ ->
+                msum $
+                  (goType mempty =<< focusType' ez) -- NB: no binders in term scope over a type child
+                    : map (go mempty) (exprChildren opts dez)
     goType :: Cxt -> TypeZ -> f a
     goType lets tz =
       extract.ty tz lets
         <|> case target tz of
           TLet _ a t _body
             -- Prefer to compute inside the body of a let, but otherwise compute in the binding
-            | [tz', bz] <- typeChildren tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType mempty tz'
-          _ -> msum $ map (goType mempty) $ typeChildren tz
+            | [tz', bz] <- typeChildren UnderBinders tz -> goType (cxtAddLet (LetTyBind $ LetTypeBind a t) lets) bz <|> goType mempty tz'
+          _ -> msum $ map (goType mempty) $ typeChildren opts tz
 
 data FMExpr m = FMExpr
   { expr :: ExprZ -> Dir -> Cxt -> m
@@ -149,17 +170,19 @@ focusType' = maybe empty pure . focusType
 findRedex ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  NormalOrderOptions ->
   ViewRedexOptions ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   MaybeT m RedexWithContext
-findRedex opts tydefs globals =
+findRedex optsN optsV tydefs globals =
   foldMapExpr
+    optsN
     ( FMExpr
-        { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex opts tydefs globals d (target ez))
-        , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType opts (target tz))
+        { expr = \ez d -> runReaderT (RExpr ez <$> viewRedex optsV tydefs globals d (target ez))
+        , ty = \tz -> hoistMaybe . runReader (RType tz <<$>> viewRedexType optsV (target tz))
         }
     )
 
@@ -168,8 +191,8 @@ children' z = case down z of
   Nothing -> mempty
   Just z' -> z' : unfoldr (fmap (\x -> (x, x)) . right) z'
 
-exprChildren :: (Dir, ExprZ) -> [(Dir, ExprZ)]
-exprChildren (d, ez) =
+exprChildren' :: (Dir, ExprZ) -> [(Dir, ExprZ)]
+exprChildren' (d, ez) =
   children' ez <&> \c -> do
     let d' = case target ez of
           App _ f _ | f == target c -> Syn
@@ -188,8 +211,30 @@ exprChildren (d, ez) =
           _ -> Chk
     (d', c)
 
-typeChildren :: TypeZ -> [TypeZ]
-typeChildren = children'
+-- Extract the children of the current focus, except those under an binder.
+-- This is used to restrict our evaluation to "closed evaluation".
+-- NB: for consistency we skip all case branches, not just those that bind a variable.
+exprChildrenClosed :: (Dir, ExprZ) -> [(Dir, ExprZ)]
+exprChildrenClosed (d, ez) = case target ez of
+  Lam{} -> []
+  LAM{} -> []
+  Let{} -> take 1 $ exprChildren' (d, ez) -- just the binding
+  LetType{} -> []
+  Letrec{} -> []
+  Case{} -> take 1 $ exprChildren' (d, ez) -- just the scrutinee
+  _ -> exprChildren' (d, ez)
+
+exprChildren :: NormalOrderOptions -> (Dir, ExprZ) -> [(Dir, ExprZ)]
+exprChildren = \case
+  UnderBinders -> exprChildren'
+  StopAtBinders -> exprChildrenClosed
+
+typeChildren :: NormalOrderOptions -> TypeZ -> [TypeZ]
+typeChildren = \case
+  UnderBinders -> children'
+  StopAtBinders -> \tz -> case target tz of
+    TForall{} -> []
+    _ -> children' tz
 
 singletonCxt :: LetBinding -> Cxt
 singletonCxt l = Cxt [l]
diff --git a/primer/src/Primer/EvalFull.hs b/primer/src/Primer/EvalFull.hs
index 5e9166e1b..fdc7fd7bc 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 (..),
@@ -51,8 +51,18 @@ newtype EvalFullError
 type TerminationBound = Natural
 
 -- A naive implementation of normal-order reduction
-evalFull :: MonadEval l m => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
-evalFull optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsV optsR tydefs env n d expr
+evalFull ::
+  MonadEval l m =>
+  NormalOrderOptions ->
+  ViewRedexOptions ->
+  RunRedexOptions ->
+  TypeDefMap ->
+  DefMap ->
+  TerminationBound ->
+  Dir ->
+  Expr ->
+  m (Either EvalFullError Expr)
+evalFull optsN optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsN optsV optsR tydefs env n d expr
 
 -- | As 'evalFull', but also returns how many reduction steps were taken.
 -- (This is mostly useful for testing purposes.)
@@ -64,6 +74,7 @@ evalFull optsV optsR tydefs env n d expr = snd <$> evalFullStepCount optsV optsR
 -- more to notice termination.
 evalFullStepCount ::
   MonadEval l m =>
+  NormalOrderOptions ->
   ViewRedexOptions ->
   RunRedexOptions ->
   TypeDefMap ->
@@ -72,20 +83,29 @@ evalFullStepCount ::
   Dir ->
   Expr ->
   m (Natural, Either EvalFullError Expr)
-evalFullStepCount optsV optsR tydefs env n d = go 0
+evalFullStepCount optsN optsV optsR tydefs env n d = go 0
   where
     go s expr
       | s >= n = pure (s, Left $ TimedOut expr)
       | otherwise =
-          runMaybeT (step optsV optsR tydefs env d expr) >>= \case
+          runMaybeT (step optsN optsV optsR 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 => ViewRedexOptions -> RunRedexOptions -> TypeDefMap -> DefMap -> Dir -> Expr -> MaybeT m Expr
-step optsV optsR tydefs g d e =
-  findRedex optsV tydefs g d e >>= \case
+step ::
+  MonadEval l m =>
+  NormalOrderOptions ->
+  ViewRedexOptions ->
+  RunRedexOptions ->
+  TypeDefMap ->
+  DefMap ->
+  Dir ->
+  Expr ->
+  MaybeT m Expr
+step optsN optsV optsR tydefs g d e =
+  findRedex optsN optsV tydefs g d e >>= \case
     RExpr ez r -> lift $ unfocusExpr . flip replace ez . fst <$> runRedex optsR r
     RType et r -> lift $ unfocusExpr . unfocusType . flip replace et . fst <$> runRedexTy optsR r
diff --git a/primer/test/Tests/Eval/Utils.hs b/primer/test/Tests/Eval/Utils.hs
index 8cb166a68..faacda104 100644
--- a/primer/test/Tests/Eval/Utils.hs
+++ b/primer/test/Tests/Eval/Utils.hs
@@ -4,6 +4,7 @@ module Tests.Eval.Utils (
   genDirTm,
   testModules,
   hasTypeLets,
+  hasHoles,
 ) where
 
 import Foreword
@@ -15,12 +16,12 @@ import Hedgehog (PropertyT)
 import Hedgehog.Gen qualified as Gen
 import Primer.Core (
   Expr,
-  Expr' (LetType),
+  Expr' (EmptyHole, Hole, LetType),
   ID,
   Kind' (KType),
   ModuleName (ModuleName),
   Type,
-  Type' (TLet),
+  Type' (TEmptyHole, THole, TLet),
  )
 import Primer.Core.DSL (create', lam, lvar, tcon, tfun)
 import Primer.Core.Utils (forgetMetadata, forgetTypeMetadata, generateIDs)
@@ -98,3 +99,12 @@ hasTypeLets e =
   not $
     null [() | LetType{} <- universe e]
       && null [() | TLet{} <- universeBi @_ @Type e]
+
+-- | Does this expression have any holes?
+hasHoles :: Expr -> Bool
+hasHoles e =
+  not $
+    null [() | Hole{} <- universe e]
+      && null [() | EmptyHole{} <- universe e]
+      && null [() | THole{} <- universeBi @_ @Type e]
+      && null [() | TEmptyHole{} <- universeBi @_ @Type e]
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index 03342b48e..37f55d620 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,
@@ -42,16 +42,18 @@ import Primer.Core.DSL
 import Primer.Core.Utils (
   exprIDs,
   forgetMetadata,
+  generateIDs,
  )
 import Primer.Def (DefMap)
 import Primer.Eval
 import Primer.EvalFull
 import Primer.Examples qualified as Examples (
   even,
+  map,
   map',
   odd,
  )
-import Primer.Gen.Core.Typed (WT, forAllT, isolateWT, propertyWT)
+import Primer.Gen.Core.Typed (WT, forAllT, genChk, isolateWT, propertyWT)
 import Primer.Log (runPureLogT)
 import Primer.Module (
   Module (Module, moduleDefs, moduleName, moduleTypes),
@@ -120,7 +122,7 @@ import Tasty (
  )
 import Test.Tasty.HUnit (Assertion, assertBool, assertFailure, (@?=))
 import Tests.Action.Prog (readerToState)
-import Tests.Eval.Utils (genDirTm, hasTypeLets, testModules, (~=))
+import Tests.Eval.Utils (genDirTm, hasHoles, hasTypeLets, testModules, (~=))
 import Tests.Gen.Core.Typed (checkTest)
 import Tests.Typecheck (runTypecheckTestM, runTypecheckTestMWithPrims)
 
@@ -425,6 +427,25 @@ unit_15 =
         s <- evalFullTest maxID builtinTypes mempty (fromIntegral $ length steps) Syn expr
         s <~==> Right expected
 
+unit_map_hole :: Assertion
+unit_map_hole =
+  let n = 3
+      modName = mkSimpleModuleName "TestModule"
+      ((globals, expr, expected), maxID) = create $ do
+        (mapName, mapDef) <- Examples.map modName
+        let lst = list_ $ take n $ iterate (con1 cSucc) (con0 cZero)
+        e <- gvar mapName `aPP` tcon tNat `aPP` tcon tBool `app` emptyHole `app` lst
+        let globs = [(mapName, mapDef)]
+        expect <- list_ (take n $ ((emptyHole `ann` (tcon tNat `tfun` tcon tBool)) `app`) <$> iterate (con1 cSucc) (con0 cZero)) `ann` (tcon tList `tapp` tcon tBool)
+        pure (M.fromList globs, e, expect)
+   in do
+        sO <- evalFullTest maxID builtinTypes globals 200 Syn expr
+        sO <~==> Right expected
+        sCG <- evalFullTestClosed GroupedLets maxID builtinTypes globals 200 Syn expr
+        sCG <~==> Right expected
+        sCS <- evalFullTestClosed SingleLets maxID builtinTypes globals 300 Syn expr
+        sCS <~==> Right expected
+
 unit_hole_ann_case :: Assertion
 unit_hole_ann_case =
   let (tm, maxID) = create $ hole $ ann (case_ emptyHole []) (tcon tBool)
@@ -566,6 +587,235 @@ unit_tlet_self_capture = do
         r <~==> expect
    in mapM_ test (zip [0 ..] expected)
 
+-- When doing closed eval (i.e. don't go under binders), pushing a @let@
+-- through a binder is not considered to be "under" that binder, else
+-- @(let x=t1 in λy.t2 : S -> T) t3@ would be stuck.
+unit_closed_let_beta :: Assertion
+unit_closed_let_beta =
+  let ((expr, expected), maxID) = create $ do
+        e0 <-
+          let_
+            "x"
+            (con0 cFalse `ann` tcon tBool)
+            ( lam "y" (con cCons [lvar "x", lvar "y"])
+                `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))
+            )
+            `app` con0 cTrue
+        e1 <-
+          let_
+            "x"
+            (con0 cFalse `ann` tcon tBool)
+            ( lam
+                "y"
+                (con cCons [lvar "x", lvar "y"])
+            )
+            `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))
+            `app` con0 cTrue
+        e2 <-
+          lam
+            "y"
+            ( let_
+                "x"
+                (con0 cFalse `ann` tcon tBool)
+                (con cCons [lvar "x", lvar "y"])
+            )
+            `ann` (tcon tBool `tfun` (tcon tList `tapp` tcon tBool))
+            `app` con0 cTrue
+        e3 <-
+          let_
+            "y"
+            (con0 cTrue `ann` tcon tBool)
+            ( let_
+                "x"
+                (con0 cFalse `ann` tcon tBool)
+                (con cCons [lvar "x", lvar "y"])
+            )
+            `ann` (tcon tList `tapp` tcon tBool)
+        e4 <-
+          con
+            cCons
+            [ let_
+                "x"
+                (con0 cFalse `ann` tcon tBool)
+                (lvar "x")
+            , let_
+                "y"
+                (con0 cTrue `ann` tcon tBool)
+                (lvar "y")
+            ]
+            `ann` (tcon tList `tapp` tcon tBool)
+        e5 <-
+          con
+            cCons
+            [ con0 cFalse `ann` tcon tBool
+            , let_
+                "y"
+                (con0 cTrue `ann` tcon tBool)
+                (lvar "y")
+            ]
+            `ann` (tcon tList `tapp` tcon tBool)
+        e6 <-
+          con
+            cCons
+            [ con0 cFalse
+            , let_
+                "y"
+                (con0 cTrue `ann` tcon tBool)
+                (lvar "y")
+            ]
+            `ann` (tcon tList `tapp` tcon tBool)
+        e7 <-
+          con
+            cCons
+            [ con0 cFalse
+            , con0 cTrue `ann` tcon tBool
+            ]
+            `ann` (tcon tList `tapp` tcon tBool)
+        e8 <-
+          con
+            cCons
+            [ con0 cFalse
+            , con0 cTrue
+            ]
+            `ann` (tcon tList `tapp` tcon tBool)
+        pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4, e5, e6, e7, e8] ++ [Right e8])
+      test (n, expect) = do
+        r <- evalFullTestClosed GroupedLets maxID mempty mempty n Syn expr
+        r <~==> expect
+   in mapM_ test (zip [0 ..] expected)
+
+-- Closed eval and handling groups of @let@s singlely work together
+unit_closed_single_lets :: Assertion
+unit_closed_single_lets =
+  let ((expr, expected), maxID) = create $ do
+        e0 <-
+          let_ "x" (con0 cFalse) $
+            let_ "y" (con0 cTrue) $
+              con
+                cMakePair
+                [ lvar "x"
+                , lvar "y"
+                ]
+        e1 <-
+          let_ "x" (con0 cFalse) $
+            con
+              cMakePair
+              [ lvar "x"
+              , let_ "y" (con0 cTrue) $ lvar "y"
+              ]
+        e2 <-
+          con
+            cMakePair
+            [ let_ "x" (con0 cFalse) $ lvar "x"
+            , let_ "y" (con0 cTrue) $ lvar "y"
+            ]
+        e3 <-
+          con
+            cMakePair
+            [ con0 cFalse
+            , let_ "y" (con0 cTrue) $ lvar "y"
+            ]
+        e4 <-
+          con
+            cMakePair
+            [ con0 cFalse
+            , con0 cTrue
+            ]
+        pure (e0, map (Left . TimedOut) [e0, e1, e2, e3, e4] ++ [Right e4])
+      test (n, expect) = do
+        r <- evalFullTestClosed SingleLets maxID mempty mempty n Syn expr
+        r <~==> expect
+   in mapM_ test (zip [0 ..] expected)
+
+-- One reason for not evaluating under binders is to avoid a size blowup when
+-- evaluating a recursive definition. For example, the unsaturated
+-- `map @Bool @Bool not` would keep unrolling the recursive mentions of `map`.
+-- (If it were applied to a concrete list, the beta redexes would be reduced instead.)
+-- Since top-level definitions and recursive lets are essentially the same, one may
+-- worry that we have the same issue with @letrec@. This test shows that closed eval
+-- handles that case also.
+unit_closed_letrec_binder :: Assertion
+unit_closed_letrec_binder =
+  let ((expr, expected), maxID) = create $ do
+        e0 <-
+          letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $
+            lam "y" $
+              lvar "x"
+        e1 <-
+          lam "y" $
+            letrec "x" (list_ [lvar "x", lvar "x"]) (tcon tBool) $
+              lvar "x"
+        pure (e0, map (Left . TimedOut) [e0, e1] ++ [Right e1])
+      test (n, expect) = do
+        r <- evalFullTestClosed GroupedLets maxID mempty mempty n Syn expr
+        r <~==> expect
+   in mapM_ test (zip [0 ..] expected)
+
+-- closed eval stops at binders
+unit_closed_binders :: Assertion
+unit_closed_binders = do
+  let isNormalIffClosed e = do
+        let (e', i) = create e
+        evalFullTestClosed GroupedLets i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> assertFailure $ "not normal form, for closed eval, grouped lets: " <> show e'
+          Right _ -> pure ()
+        evalFullTestClosed SingleLets i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> assertFailure $ "not normal form, for closed eval, single lets: " <> show e'
+          Right _ -> pure ()
+        evalFullTest i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> pure ()
+          Right _ -> assertFailure $ "unexpectedly a normal form, for open eval: " <> show e'
+      r = let_ "x" emptyHole $ lvar "x"
+  isNormalIffClosed $ lam "x" r
+  isNormalIffClosed $ lAM "a" r
+  isNormalIffClosed $ case_ emptyHole [branch cTrue [("x", Nothing)] r]
+  -- For consistency, we also do not reduce inside case branches even if they do not bind
+  isNormalIffClosed $ case_ emptyHole [branch cTrue [] r]
+
+-- closed eval still pushes lets through binders
+unit_closed_subst :: Assertion
+unit_closed_subst = do
+  let isReducible e = do
+        let (e', i) = create e
+        evalFullTestClosed GroupedLets i mempty mempty 1 Syn e' >>= \case
+          Left (TimedOut _) -> pure ()
+          Right _ -> assertFailure $ "unexpectedly a normal form: " <> show e'
+      l = let_ "x" emptyHole
+      v = lvar "x"
+  isReducible $ l $ lam "y" v
+  isReducible $ l $ lAM "a" v
+  isReducible $ l $ case_ emptyHole [branch cTrue [("x", Nothing)] v]
+  isReducible $ l $ case_ emptyHole [branch cTrue [] v]
+
+-- For (closed, hole free) terms of base types, open and closed evaluation
+-- agree.  We require hole-free-ness, as holes create stuck terms similar to
+-- free variables. Note that we get the same reduction sequence, not only that
+-- they reduce to the same value.
+tasty_open_closed_agree_base_types :: Property
+tasty_open_closed_agree_base_types = withDiscards 1000 $
+  propertyWT testModules $ do
+    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+    let optsR = RunRedexOptions{pushAndElide = True}
+    ty <- forAllT $ Gen.element @[] [tBool, tNat, tInt]
+    tm' <- forAllT $ genChk $ TCon () ty
+    tm <- generateIDs tm'
+    when (hasHoles tm) discard
+    tds <- asks typeDefs
+    let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
+    let reductionSequence closed expr n =
+          (expr :)
+            <$> if n <= (0 :: Integer)
+              then pure []
+              else
+                evalFull @EvalLog closed optsV optsR tds globs 1 Chk expr >>= \case
+                  Left (TimedOut expr') -> reductionSequence closed expr' (n - 1)
+                  Right _ -> pure []
+    (openSeq, openLogs) <- lift $ isolateWT $ runPureLogT $ reductionSequence UnderBinders tm 100
+    testNoSevereLogs openLogs
+    (closedSeq, closedLogs) <- lift $ isolateWT $ runPureLogT $ reductionSequence StopAtBinders tm 100
+    testNoSevereLogs closedLogs
+    openSeq === closedSeq
+
 -- TODO: examples with holes
 
 -- TODO: most of these property tests could benefit from generating an
@@ -588,6 +838,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.frequency [(10, pure UnderBinders), (1, pure StopAtBinders)]
   -- 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
@@ -595,19 +846,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 optsV optsR tds globs n dir t
+  ((stepsFinal', sFinal), logs) <- lift $ isolateWT $ runPureLogT $ evalFullStepCount @EvalLog closed optsV optsR 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 optsV optsR tds globs m dir t
+  (stepsMid, sMid') <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR 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 optsV optsR tds globs (stepsFinal - m) dir sMid
+  (stepsTotal, sTotal) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs (stepsFinal - m) dir sMid
   stepsMid + stepsTotal === stepsFinal'
   sFinal === sTotal
 
@@ -1015,7 +1266,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 optsV optsR tds globs maxSteps dir t
+      closed <- forAllT $ Gen.frequency [(10, pure UnderBinders), (1, pure StopAtBinders)]
+      (steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs maxSteps dir t
       annotateShow steps
       annotateShow s
       -- s is often reduced to normal form
@@ -1025,7 +1277,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 optsV optsR tds globs midSteps dir t
+          (_, s') <- failWhenSevereLogs $ evalFullStepCount @EvalLog closed optsV optsR tds globs midSteps dir t
           test "mid " s'
 
 -- Unsaturated primitives are stuck terms
@@ -1483,6 +1735,7 @@ unit_eval_full_modules =
                 { evalFullReqExpr = foo
                 , evalFullCxtDir = Chk
                 , evalFullMaxSteps = 2
+                , evalFullOptions = UnderBinders
                 }
         expect <- char 'A'
         pure $ case resp of
@@ -1505,8 +1758,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"
@@ -1535,10 +1793,11 @@ tasty_unique_ids = withTests 1000 $
       let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
       tds <- asks typeDefs
       (dir, t1, _) <- genDirTm
+      closed <- forAllT $ Gen.frequency [(10, pure UnderBinders), (1, pure StopAtBinders)]
       let go n t
             | n == (0 :: Int) = pure ()
             | otherwise = do
-                t' <- failWhenSevereLogs $ evalFull @EvalLog optsV optsR tds globs 1 dir t
+                t' <- failWhenSevereLogs $ evalFull @EvalLog closed optsV optsR tds globs 1 dir t
                 case t' of
                   Left (TimedOut e) -> uniqueIDs e >> go (n - 1) e
                   Right e -> uniqueIDs e
@@ -1606,9 +1865,10 @@ unit_case_prim =
 
 evalFullTest :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
 evalFullTest id_ tydefs globals n d e = do
+  let optsN = UnderBinders
   let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
   let optsR = RunRedexOptions{pushAndElide = True}
-  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e
   assertNoSevereLogs logs
   distinctIDs r
   pure r
@@ -1624,11 +1884,27 @@ evalFullTestExactSteps id_ tydefs globals n d e = do
         Left t' -> assertFailure $ "Unexpected timeout: " <> show t'
         Right t' -> pure t'
 
+data GroupedLets = GroupedLets | SingleLets
+
+evalFullTestClosed :: GroupedLets -> ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
+evalFullTestClosed gl id_ tydefs globals n d e = do
+  let optsN = StopAtBinders
+  let gl' = case gl of
+        GroupedLets -> True
+        SingleLets -> False
+  let optsV = ViewRedexOptions{groupedLets = gl', aggressiveElision = True}
+  let optsR = RunRedexOptions{pushAndElide = True}
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR 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 optsN = UnderBinders
   let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
   let optsR = RunRedexOptions{pushAndElide = True}
-  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsV optsR tydefs globals n d e
+  let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR 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 e36bdedd3..aee0c7048 100644
--- a/primer/test/Tests/Prelude/Utils.hs
+++ b/primer/test/Tests/Prelude/Utils.hs
@@ -8,6 +8,7 @@ import Optics (over)
 import Primer.Core (Expr, GVarName, Type)
 import Primer.Core.DSL (apps', create', gvar)
 import Primer.Eval (
+  NormalOrderOptions (UnderBinders),
   RunRedexOptions (RunRedexOptions, pushAndElide),
   ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets),
  )
@@ -53,11 +54,12 @@ functionOutput f args = functionOutput' f (map Left args)
 -- Tests a prelude function with a combination of Expr/Type arguments to be applied
 functionOutput' :: GVarName -> [Either (TestM Expr) (TestM Type)] -> TerminationBound -> Either EvalFullError Expr
 functionOutput' f args depth =
-  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+  let optsN = UnderBinders
+      optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
       optsR = RunRedexOptions{pushAndElide = True}
       (r, logs) = evalTestM 0 $ runPureLogT $ do
         e <- apps' (gvar f) $ bimap lift lift <$> args
-        evalFull @EvalLog optsV optsR ty def n d e
+        evalFull @EvalLog optsN optsV optsR 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