GoalState.withContext should allow lifting #171

New Issue

aniva · 2025-03-08T20:45:40-08:00

aniva commented

2025-03-08 20:45:40 -08:00

We can define it like this instead:

protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α :=
  Meta.mapMetaM <| state.withContext mvarId

We can define it like this instead: ```lean protected def GoalState.withContext { m } [MonadControlT MetaM m] [Monad m] (state: GoalState) (mvarId: MVarId) : m α → m α := Meta.mapMetaM <| state.withContext mvarId ```

aniva added this to the 0.3 milestone 2025-03-08 20:45:40 -08:00

aniva added the

labels 2025-03-08 20:45:40 -08:00

aniva self-assigned this 2025-03-08 20:45:40 -08:00

aniva added a new dependency 2025-03-08 21:04:55 -08:00

#169 chore: Cleanup the library system

aniva referenced this issue

2025-03-08 21:07:05 -08:00