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.clearExcept : Lean.ParserDescr

Clears all hypotheses it can besides those provided

Equations

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