diff --git a/Repl.lean b/Repl.lean
index a735c88..9dd9f80 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -81,6 +81,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
     : EMainM α := do
   let scope := (← get).scope
   let context := {
+    errToSorry := false,
     isNoncomputableSection := scope.isNoncomputable,
   }
   let state := {