issue !4#9129: `mk_iff` and `ext` add too many explicit a...

Stream: triage

[Random Issue Bot]

Today I chose issue 9129 for discussion!

mk_iff and ext add too many explicit arguments
Created by @Yaël Dillies (@YaelDillies) on 2023-12-17
Labels: t-meta

Is this issue still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

@Yury G. Kudryashov, haven't you fixed all three items now?

[Yury G. Kudryashov]

ext was fixed by someone else. Link doesn't work on my phone. What's the third item?

[Yury G. Kudryashov]

mk_iff still uses explicit arguments. I can fix it tomorrow.

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/Recent.20Commits.20to.20lean4.3Amaster/near/449969799 should be the Lean change

[Yury G. Kudryashov]

For mk_iff, I only fixed lower/uppercase.

[Yury G. Kudryashov]

I checked the second checkbox.