clear

clear erases assumptions from the assumption space. Multiple assumptions may be erased in one tactic via a space-separated list of assumptions. clear will fail if an assumption passed into it contains as subterms other variables that still exist in the goal state.

Syntax

(* Simple usage *)
clear H.

(* Clear multiple assumptions *)
clear H Heq X Y n.

Examples

Before

n: nat
H, Hr1, Hr2: n = 0
IHn: n = 1
-------------------------
1/1
False

clear Hr1 Hr2.

After

n: nat
H: n = 0
IHn: n = 1
-------------------------
1/1
False

Resources

Reference Documentation

---