Zulip Chat Archive
Stream: general
Topic: mk_iff tactic
Yury G. Kudryashov (Dec 31 2023 at 02:12):
I'm reading the source of mk_iff, and I'm going to ask many questions about it here. First question: am I right that Mathlib.Tactic.MkIff.select here applies left only once (as it probably should if the goal is a ∨ b ∨ c ∨ ...)?
Mario Carneiro (Dec 31 2023 at 02:17):
that looks like a bug, from the docs
Yury G. Kudryashov (Dec 31 2023 at 02:18):
My guess is that the docs are bogus and the code is correct.
Mario Carneiro (Dec 31 2023 at 02:18):
yes, if it's an iterated or then we would expect only one left
Junyan Xu (Dec 31 2023 at 07:17):
Currently mk_iff generates the name IsLocalization_iff for the Prop-valued class IsLocalization, but it should be isLocalization_iff according to naming convention, and I have to specify the name manually. Should I file a bug?
Yaël Dillies (Dec 31 2023 at 07:59):
I already opened an issue about this
Yaël Dillies (Dec 31 2023 at 08:00):
Yury G. Kudryashov (Dec 31 2023 at 16:32):
I'll try to fix it today.
Yury G. Kudryashov (Dec 31 2023 at 16:32):
(let it be my simple exercise on meta programming)
Last updated: May 02 2025 at 03:31 UTC