Cardinal.mk'_def

Stream: mathlib4

[Violeta Hernández]

Why does docs#Cardinal.mk'_def have a prime in its name? Is this some sort of porting oversight?

[Ruben Van de Velde]

Is ⟦α⟧ not Quotient.mk'?

[Violeta Hernández]

Yes, but #α is Cardinal.mk

[Ruben Van de Velde]

Oh no, it's Quotient.mk too

[Ruben Van de Velde]

And it was cardinal.mk_def in ml3

[Ruben Van de Velde]

Per #2084, mathport came up with it

[Violeta Hernández]

I'll deprecate this name and switch it back to Cardinal.mk_def, then

[Ruben Van de Velde]

Oh right, I think I remember what went wrong. quotient.mk used an instance argument, so it matched Quotient.mk', but we also changed the meaning of the syntax to the variant that didn't use an instance argument during the port

[Ruben Van de Velde]

Heh: -- Porting note: cardinal.mk_def is now Cardinal.mk'_def, not sure why

[Ruben Van de Velde]

@Violeta Hernández actually I'll propose deprecating it outright, PR incoming

[Violeta Hernández]

Yeah, I think it can be deprecated. Its only usages are in proofs using Quotient.inductionOn, which can be replaced by Cardinal.inductionOn.

[Ruben Van de Velde]

#18205, let's see if simp was using it anywhere

[Ruben Van de Velde]

That'll be for tomorrow, though

[Ruben Van de Velde]

(Feel free to push to that PR if needed)