Documentation

Mathlib.Tactic.ClearExcept

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.

source
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).

Instances For
    source
    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).

    Instances For
      source
      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.

      Instances For