aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 14 Pull Requests 2 Packages Projects Releases Wiki Activity

fix(repl): Elaborate with `errToSorry` as false by default

This commit is contained in:
Leni Aniva 2025-04-10 23:13:35 -07:00
parent c547d9c8dc
commit 14b74b612d
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Repl.lean
View File

@ -81,6 +81,7 @@ def liftTermElabM { α } (termElabM: Elab.TermElabM α) (levelNames : List Name
: EMainM α := do : EMainM α := do
let scope := (← get).scope let scope := (← get).scope
let context := { let context := {
errToSorry := false,
isNoncomputableSection := scope.isNoncomputable, isNoncomputableSection := scope.isNoncomputable,
} }
let state := { let state := {