@[inline, reducible]

abbrev Lean.MVarId.cleanup (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Auxiliary tactic for cleaning the local context. It removes local declarations (aka hypotheses) that are not relevant. We say a variable x is "relevant" if

• It occurs in the target type, or
• There is a relevant variable y that depends on x, or
• The type of x is a proposition and it depends on a relevant variable y.

Equations

• Lean.MVarId.cleanup mvarId = Lean.Meta.cleanupCore mvarId

@[inline, reducible, deprecated Lean.MVarId.cleanup]

abbrev Lean.Meta.cleanup (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Equations

• Lean.Meta.cleanup mvarId = Lean.MVarId.cleanup mvarId