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):
clear doesn't work if the goal depends on
Rob Lewis (Sep 04 2020 at 12:18):
Last updated: May 13 2021 at 20:13 UTC