From 4042ec707ee8a0eaec685c9b71812d62bc120d59 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 7 Sep 2024 13:54:52 -0700 Subject: [PATCH] refactor: Use `Meta.mapMetaM` --- Pantograph/Goal.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 1c2bf8d..0109204 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -71,10 +71,10 @@ protected def GoalState.metaState (state: GoalState): Meta.State := protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do mvarId.withContext m |>.run' (← read) state.metaState -protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do - state.withContext state.parentMVar?.get! m -protected def GoalState.withRootContext (state: GoalState) (m: MetaM α): MetaM α := do - state.withContext state.root m +protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := + Meta.mapMetaM <| state.withContext state.parentMVar?.get! +protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α := + Meta.mapMetaM <| state.withContext state.root private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k