Tactic: clear

The clear tactic can be used with any goal to remove hypotheses and variables from the context. This is useful to simplify the context by removing assumptions and variables that are no longer needed.

There are two variants of the clear tactic: an opt-in variant where specific hypotheses and variables are removed, and an opt-out variant where all hypotheses and variables except for the specified ones are removed.

Syntax

clear

When given no arguments, the clear tactic removes all hypotheses and all variables not transitively used in the goal from the context.

Syntax

clear -{idents}

Here, {idents} is a non-empty space separated list of identifiers of the hypotheses and variables that should not be cleared. The tactic removes all hypotheses and variables except for those in the list, and those used transitively in the goal or in the objects in the list.

Syntax

clear {idents}

Here, {idents} is a non-empty space separated list of identifiers of the hypotheses and variables to be cleared. If one of these is transitively used in the goal, then it is not cleared and an error is raised.