@[inline]

def Lean.MVarId.cleanup (mvarId : MVarId) (toPreserve : Array FVarId := #[]) (indirectProps : Bool := true) : MetaM 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 toPreserve array, or
• It occurs in the target type, or
• There is a relevant variable y that depends on x, or
• If indirectProps is true, the type of x is a proposition and it depends on a relevant variable y.
• If indirectProps is true, x is a local declartation and its value mentions a relevant variable y.

By default, toPreserve := #[] and indirectProps := true. These settings are used in the mathlib tactic extract_goal to give the user more control over which variables to include.

Equations

• mvarId.cleanup toPreserve indirectProps = Lean.Meta.cleanupCore✝ mvarId toPreserve indirectProps