def Lean.MVarId.revert (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) (preserveOrder : optParam Bool false) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Revert free variables fvarIds at goal mvarId.

Equations

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

def Lean.Meta.revert (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) (preserveOrder : optParam Bool false) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Equations

• Lean.Meta.revert mvarId fvarIds preserveOrder = Lean.MVarId.revert mvarId fvarIds preserveOrder