## Stream: general

### Topic: drop the value of a hypothesis?

#### Scott Morrison (Sep 04 2020 at 12:09):

Is there a tactic whose purpose is to drop the value of a hypothesis, keeping only its type? e.g. to replace x : nat := 5 with x : nat?

#### Scott Morrison (Sep 04 2020 at 12:11):

(I am experiencing a rfl which times out, even though the goal is a safe looking f x = f x. Usually the fix here is to make something irreducible. Here f is some interesting function constructed with a let earlier in the tactic block. I was thinking if I could drop the value that might be like making it irreducible.)

#### Scott Morrison (Sep 04 2020 at 12:12):

oh, it is not actually the rfl that causes the timeout... sorry causes the same timeout. false alarm

#### Anne Baanen (Sep 04 2020 at 12:14):

Out of curiosity: would this work?

example : false :=
begin
let x : ℕ := 5,
have x' := x,
clear x,
sorry
end


#### Anne Baanen (Sep 04 2020 at 12:15):

Nope, because clear doesn't work if the goal depends on x.

#### Rob Lewis (Sep 04 2020 at 12:18):

tactic#clear_value

Last updated: May 13 2021 at 20:13 UTC