We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
monadLift
1 parent 2fd99ce commit 1314af5Copy full SHA for 1314af5
src/Lean/Elab/Command.lean
@@ -131,7 +131,7 @@ instance : MonadLift CoreM CommandElabM where
131
monadLift x := private do
132
let ds ← getThe DerivedState
133
let (a, coreS) ← x.run ds.coreCtx ds.coreState
134
- modify fun s => s.updateCore coreS
+ set { ds with toState := ds.toState.updateCore coreS, coreState := coreS }
135
return a
136
137
protected nonrec def CommandElabM.run (ctx : Context) (s : State) (x : CommandElabM α) : EIO Exception (α × State) := do
0 commit comments