mathlib3 documentation

tactic.clear

Better clear tactics #

We define two variants of the standard clear tactic:

Implementation notes #

The implementation (ab)uses the native revert_lst, which can figure out dependencies between hypotheses. This implementation strategy was suggested by Simon Hudon.

source
meta def tactic.clear' (clear_dependent : bool) (hyps : list expr) :
tactic unit

Clears all the hypotheses in hyps. The tactic fails if any of the hyps is not a local or if the target depends on any of the hyps. It also fails if hyps contains duplicates.

If there are local hypotheses or definitions, say H, which are not in hyps but depend on one of the hyps, what we do depends on clear_dependent. If it is true, H is implicitly also cleared. If it is false, clear' fails.

source
meta def tactic.interactive.clear' (p : interactive.parse (lean.parser.many lean.parser.ident)) :
tactic unit

An improved version of the standard clear tactic. clear is sensitive to the order of its arguments: clear x y may fail even though both x and y could be cleared (if the type of y depends on x). clear' lifts this limitation.

example {α} {β : α → Type} (a : α) (b : β a) : unit :=
begin
  try { clear a b }, -- fails since `b` depends on `a`
  clear' a b,        -- succeeds
  exact ()
end
source
meta def tactic.interactive.clear_dependent (p : interactive.parse (lean.parser.many lean.parser.ident)) :
tactic unit

A variant of clear' which clears not only the given hypotheses, but also any other hypotheses depending on them.

example {α} {β : α → Type} (a : α) (b : β a) : unit :=
begin
  try { clear' a },  -- fails since `b` depends on `a`
  clear_dependent a, -- succeeds, clearing `a` and `b`
  exact ()
end
source
def tactic_doc.tactic.clear'  :
tactic_doc_entry

An improved version of the standard clear tactic. clear is sensitive to the order of its arguments: clear x y may fail even though both x and y could be cleared (if the type of y depends on x). clear' lifts this limitation.

example {α} {β : α → Type} (a : α) (b : β a) : unit :=
begin
  try { clear a b }, -- fails since `b` depends on `a`
  clear' a b,        -- succeeds
  exact ()
end