Clear all hypotheses starting with _
, like _match
and _let_match
.
Equations
- Mathlib.Tactic.clear_ = Lean.ParserDescr.node `Mathlib.Tactic.clear_ 1024 (Lean.ParserDescr.nonReservedSymbol "clear_" false)
Mathlib.Tactic.Clear_
Clear all hypotheses starting with _
, like _match
and _let_match
.