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: Aug 03 2023 at 10:10 UTC

Theme Simple by wildflame © 2016 Powered by jekyll