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.

clear - ... can also be used to erase all assumptions not depended on by a provided set of assumptions.

Syntax

(* Simple usage *)
clear H.

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

(* Clear anything that x, z, or c do not depend on *)
clear - x z c.

Examples

Before

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

clear Hr1 Hr2.

After

n: nat
H: n = 0
IHn: n = 1
=========================
1/1
True

Before

a, b, c, x, y, z: nat
H: a = z
=========================
1/1
True

clear - a x H.

After

a, x, z: nat
H: a = z
=========================
1/1
True

Resources

Reference Documentation

---