leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: general

Topic: implicit mk_iff


Yaël Dillies (Jun 30 2022 at 21:00):

Is there a way to make mk_iff generate a lemma with implicit arguments? The default behavior is to make everything explicit, and this goes against our convention of making arguments to an iff implicit.

Eric Wieser (Jun 30 2022 at 21:03):

Same for ext on structures

Eric Wieser (Jun 30 2022 at 21:11):

Sounds like it's time to learn to metaprogram, Yaël


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll