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.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 => pure mvarId

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 mvarId => Lean.MVarId.tryClear mvarId fvarId) mvarId fvarIds (Array.size fvarIds)

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