Documentation

Lean.Meta.Tactic.Clear

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

Lean.MetaM Lean.MVarId

Equations

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

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

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.tryClear mvarId fvarId = HOrElse.hOrElse (Lean.Meta.clear mvarId fvarId) fun x => pure mvarId

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

Lean.MetaM Lean.MVarId

Equations

Lean.Meta.tryClearMany mvarId fvarIds = Array.foldrM (fun fvarId mvarId => Lean.Meta.tryClear mvarId fvarId) mvarId fvarIds (Array.size fvarIds)