feat: Expose GoalState
functions #94
|
@ -71,10 +71,10 @@ protected def GoalState.metaState (state: GoalState): Meta.State :=
|
||||||
protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
|
protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
|
||||||
mvarId.withContext m |>.run' (← read) state.metaState
|
mvarId.withContext m |>.run' (← read) state.metaState
|
||||||
|
|
||||||
protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
|
protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
|
||||||
state.withContext state.parentMVar?.get! m
|
Meta.mapMetaM <| state.withContext state.parentMVar?.get!
|
||||||
protected def GoalState.withRootContext (state: GoalState) (m: MetaM α): MetaM α := do
|
protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
|
||||||
state.withContext state.root m
|
Meta.mapMetaM <| state.withContext state.root
|
||||||
|
|
||||||
private def GoalState.mvars (state: GoalState): SSet MVarId :=
|
private def GoalState.mvars (state: GoalState): SSet MVarId :=
|
||||||
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
|
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
|
||||||
|
|
Loading…
Reference in New Issue