Zulip Chat Archive

Stream: general

Topic: tfae fails

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

Mario Carneiro (Jan 30 2020 at 07:22):

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

Mario Carneiro (Jan 30 2020 at 07:26):

#1930

Yury G. Kudryashov (Jan 30 2020 at 08:28):

Thank you!

Last updated: Dec 20 2023 at 11:08 UTC