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 = Lean.MVarId.clear mvarId 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

• Lean.MVarId.tryClear mvarId fvarId = HOrElse.hOrElse (Lean.MVarId.clear mvarId 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 = Lean.MVarId.tryClear mvarId 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

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

@[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 = Lean.MVarId.tryClearMany mvarId fvarIds