Erase the given free variable from the goal mvarId
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[deprecated Lean.MVarId.clear]
Equations
- Lean.Meta.clear mvarId fvarId = mvarId.clear fvarId
Instances For
Try to erase the given free variable from the goal mvarId
. It is no-op if the free variable
cannot be erased due to forward dependencies.
Equations
- mvarId.tryClear fvarId = HOrElse.hOrElse (mvarId.clear fvarId) fun (x : Unit) => pure mvarId
Instances For
@[deprecated Lean.MVarId.tryClear]
Equations
- Lean.Meta.tryClear mvarId fvarId = mvarId.tryClear fvarId
Instances For
Try to erase the given free variables from the goal mvarId
.
Equations
- mvarId.tryClearMany fvarIds = Array.foldrM (fun (fvarId : Lean.FVarId) (mvarId : Lean.MVarId) => mvarId.tryClear fvarId) mvarId fvarIds fvarIds.size
Instances For
@[deprecated Lean.MVarId.tryClearMany]
Equations
- Lean.Meta.tryClearMany mvarId fvarIds = mvarId.tryClearMany fvarIds