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.

Equations

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

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

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

Equations

• Lean.Elab.Tactic.clearExcept preserve goal = do let toClear ← Lean.Elab.Tactic.getVarsToClear preserve goal.tryClearMany toClear

def Lean.Elab.Tactic.clearExceptTactic : ParserDescr

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

  clear * - h₁ h₂

Equations

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