2025-05-01 09:00:04 -07:00
1 changed files with 1 additions and 0 deletions
--- 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 := {