Zulip Chat Archive

Stream: general

Topic: tfae fails


view this post on Zulip Yury G. Kudryashov (Jan 30 2020 at 07:01):

Hi, the following fails at tfae_finish with some strange app_builder_exception error. Any ideas?

import tactic.tfae

lemma test_tfae (p : unit  Prop) : tfae [p (), p ()] :=
begin
  tfae_have : 1  2, from iff.rfl,
  tfae_finish
end

view this post on Zulip Mario Carneiro (Jan 30 2020 at 07:22):

It gets confused with arrows in the context and thinks they are implications for the scc

view this post on Zulip Mario Carneiro (Jan 30 2020 at 07:26):

#1930

view this post on Zulip Yury G. Kudryashov (Jan 30 2020 at 08:28):

Thank you!


Last updated: May 15 2021 at 02:11 UTC