def Lean.Meta.SavedState.runMetaM {α : Type} (s : Lean.Meta.SavedState) (x : Lean.MetaM α) : Lean.MetaM (α × Lean.Meta.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 : Lean.Meta.SavedState) (x : Lean.MetaM α) : Lean.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 : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) : Lean.MetaM (Array Lean.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 : Lean.Meta.SavedState) (postState : Lean.Meta.SavedState) : Lean.MetaM (Array Lean.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.