def Lean.Meta.SavedState.runMetaM {α : Type} (s : SavedState) (x : MetaM α) : MetaM (α × SavedState)

Run the action x in state s. Returns the result of x and the state after x was executed. The global state remains unchanged.

Equations

• s.runMetaM x = Lean.withoutModifyingState' do Lean.restoreState s x

def Lean.Meta.SavedState.runMetaM' {α : Type} (s : SavedState) (x : MetaM α) : MetaM α

Run the action x in state s. Returns the result of x. The global state remains unchanged.

Equations

• s.runMetaM' x = Lean.withoutModifyingState do Lean.restoreState s x

def Lean.Meta.getIntroducedExprMVars (preState postState : SavedState) : MetaM (Array MVarId)

Returns the mvars that are not declared in preState, but declared and unassigned in postState. Delayed-assigned mvars are considered assigned.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.getAssignedExprMVars (preState postState : SavedState) : MetaM (Array MVarId)

Returns the mvars that are declared but unassigned in preState, and assigned in postState. Delayed-assigned mvars are considered assigned.

Equations

• One or more equations did not get rendered due to their size.