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.

@[deprecated Lean.MVarId.clear]

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

Equations

• Lean.Meta.clear mvarId fvarId = mvarId.clear fvarId

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

@[deprecated Lean.MVarId.tryClear]

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

Equations

• Lean.Meta.tryClear mvarId fvarId = mvarId.tryClear fvarId

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 fvarIds.size

@[deprecated Lean.MVarId.tryClearMany]

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

Equations

• Lean.Meta.tryClearMany mvarId fvarIds = mvarId.tryClearMany fvarIds