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

Equations

• mvarId.tryClear fvarId = (mvarId.clear fvarId <|> pure mvarId)

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.

Equations

• mvarId.tryClearMany fvarIds = Array.foldrM (fun (fvarId : Lean.FVarId) (mvarId : Lean.MVarId) => mvarId.tryClear fvarId) mvarId fvarIds

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.

Equations

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