Zulip Chat Archive

Stream: general

Topic: drop the value of a hypothesis?


view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anne Baanen (Sep 04 2020 at 12:15):

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

view this post on Zulip Rob Lewis (Sep 04 2020 at 12:18):

tactic#clear_value


Last updated: May 13 2021 at 20:13 UTC