Merge pull request 'fix(repl): Elaborate with `errToSorry` as false by default' (#187 ) from repl/elab-option into dev

Reviewed-on: #187
fix(repl): Elaborate with `errToSorry` as false by default
2025-05-01 09:00:02 -07:00 · 2025-04-10 23:14:00 -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 := {
Author	SHA1	Message	Date
Leni Aniva	0a987174bc	Merge pull request 'fix(repl): Elaborate with `errToSorry` as false by default' (#187 ) from repl/elab-option into dev Reviewed-on: #187	2025-05-01 09:00:02 -07:00
Leni Aniva	14b74b612d	fix(repl): Elaborate with `errToSorry` as false by default	2025-04-10 23:14:00 -07:00