drop the value of a hypothesis?

Stream: general

[Scott Morrison]

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]

(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]

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

[Anne Baanen]

Out of curiosity: would this work?

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

[Anne Baanen]

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

[Rob Lewis]

tactic#clear_value