Pi.toLex_apply

Stream: mathlib4

[Violeta Hernández]

Might I ask what's going on with docs#Pi.toLex_apply and docs#Pi.ofLex_apply ? They both seem like flagrant def-eq abuse.

[Weiyi Wang]

It is defeq non-abuse I think. It means, as Lex-tagged function can still be used as a function, the function application result is the same regardless whether the tag is there

[Weiyi Wang]

(that's assuming function application for Lex tag is defined that way, which I have not found yet)

[Weiyi Wang]

TIL type synonym of a function / pi type will automatically expand to the underlying function for function application, which is why this is defeq.
It makes some sense to me, but I imagine you asked this question because you expect toLex f a to return something other than f a? Like toLex (f a)?

[Aaron Liu]

looks like defeq abuse to me

[Aaron Liu]

if docs#Lex was a one-field structure then it wouldn't work

[Eric Wieser]

I think we've set a precedent that application doesn't really count as defeq abuse

[Eric Wieser]

See Matrix and PiLp for more examples

[Eric Wieser]

I think the prevailing take is that we should ignore such abuse until we switch to one-field structures, for which WithLp already has a PR

[Violeta Hernández]

Shouldn't the non-abusive way to do this be to add a CoeFun α → CoeFun (Lex α) instance?

[Robin Arnez]

That won't have any effect because it will first try regular function application before CoeFun. In other words, Lex (_ -> _) can't be a function type if you want to make this work

[Violeta Hernández]

Ah, so once Lex is made into a one-element structure, that will work, right?

[Robin Arnez]

Yeah, and until then there's not much we can do