Documentation

Lean.Meta.Tactic.Cleanup

@[inline, reducible]

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
Instances For
    @[inline, reducible, deprecated Lean.MVarId.cleanup]
    Equations
    Instances For