implicit mk_iff

Stream: general

[Yaël Dillies]

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]

Same for ext on structures

[Eric Wieser]

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