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

Erase the given free variable from the goal mvarId.

def Lean.MVarId.tryClear (mvarId : MVarId) (fvarId : FVarId) : MetaM 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.

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

Try to clear the given fvars from the local context.

The fvars must be given in the order they appear in the local context.

See also tryClearMany' which takes care of reordering internally, and returns the cleared hypotheses along with the new goal.

def Lean.MVarId.tryClearMany' (goal : MVarId) (fvarIds : Array FVarId) : MetaM (MVarId × Array FVarId)

Try to clear the given fvars from the local context. Returns the new goal and the hypotheses that were cleared.

Does not require the hyps to be given in the order in which they appear in the local context.