def Lean.MVarId.clear (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM Lean.MVarId

Erase the given free variable from the goal mvarId.

Equations

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

def Lean.MVarId.tryClear (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM Lean.MVarId

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

def Lean.MVarId.tryClearMany (mvarId : Lean.MVarId) (fvarIds : Array Lean.FVarId) : Lean.MetaM Lean.MVarId

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