FunLike-classes

Stream: mathlib4

[Antoine Chambert-Loir]

If a class myClass depends on a [Funlike F X Y] hypothesis, should it implement myClass.ext_iff (which would be defined as DFunLike.ext_iff …) etc., or should the user simply rely on docs#DFunLike.ext_iff ?

[Antoine Chambert-Loir]

Trying to answer my question myself : it seems myClass.ext_iff should not be added.
On the other hand, docs#MonoidHom.ext_iff is tagged as deprecated, while docs#LinearMap.ext_iff isn't.

[Yaël Dillies]

I don't think it matters much. It's better to copy it for discoverability, but no biggie

[Antoine Chambert-Loir]

OK. I understood the issue I had. Defining myHomClass.ext_iff … [FunLike F X Y] [myHomClass F X Y] makes the unusedArguments linter complain, because that function only uses [FunLike F X Y]. So it seems that for the class, one has to use docs#FunLike.ext_iff. However, this works for the type version, one can define myHom.ext_iff (f : myHom X Y), although some cases are marked as deprecated in mathlib.

[Yaël Dillies]

Ah yes, that's a funny consequence of the new design that I hadn't foreseen.

[Kevin Buzzard]

I thought the whole point of the set-up was to save the user from having to write a new ext_iff lemma?

[Anne Baanen]

Only MyHom.ext needs to be defined (for the @[ext] attribute to work). MyHom.ext_iff as alias for DFunLike.ext_iff is possible if you really want dot notation but as Kevin said it duplicates work. I am against MyHomClass.ext_iff, since the subclassing adds nothing that the original DFunLike.ext_iff can't do (and now with FunLike moving to a separate parameter, the linter rightfully complains!)