Zulip Chat Archive
Stream: general
Topic: Buggy interaction between `refine` and `resetI`
Markus Himmel (Aug 14 2020 at 19:00):
Is this a known bug?
import tactic.cache
class foo :=
(a : ℕ)
example : foo → foo :=
begin
intro h,
resetI,
apply_instance -- works
end
example : foo → foo :=
begin
refine λ h, _,
resetI,
apply_instance,
/-
tactic.mk_instance failed to generate instance for
foo
state:
h : foo
⊢ foo
-/
end
Kenny Lau (Aug 14 2020 at 19:12):
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/refine.20and.20resetI
Last updated: Dec 20 2023 at 11:08 UTC