From 14b74b612ddbe89af4dbde27e5e9e6ffd17b7e45 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 10 Apr 2025 23:13:35 -0700
Subject: [PATCH] fix(repl): Elaborate with `errToSorry` as false by default

---
 Repl.lean | 1 +
 1 file changed, 1 insertion(+)

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 := {