Zulip Chat Archive

Stream: general

Topic: Buggy interaction between `refine` and `resetI`


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

view this post on Zulip Kenny Lau (Aug 14 2020 at 19:12):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/refine.20and.20resetI


Last updated: May 16 2021 at 05:21 UTC