The clear* tactic

This file provides a variant of the clear tactic, which clears all hypotheses it can besides a provided list.

def Lean.Elab.Tactic.getVarsToClear (preserve : Array FVarId) : MetaM (Array FVarId)

Returns the free variable IDs that can be cleared, excluding those in the preserve list and class instances.

def Lean.Elab.Tactic.clearExcept (preserve : Array FVarId) (goal : MVarId) : MetaM MVarId

Clears all hypotheses from a goal except those in the preserve list.

def Lean.Elab.Tactic.clearExceptTactic : ParserDescr

Clears all hypotheses it can, except those provided after a minus sign. Example:

  clear * - h₁ h₂