The clear* tactic

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

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, class instances, and auxiliary declarations (e.g. recursive hypotheses).

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, class instances, and auxiliary declarations (e.g. recursive hypotheses).

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, class instances, and hidden auxiliary declarations (for example recursive hypotheses). Example:

  clear * - h₁ h₂

The intent is that clear * - only clears user-visible local declarations; hidden auxiliary declarations should be handled by more specific mechanisms when needed.

Equations

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