PartENat

Stream: mathlib4

[Jireh Loreaux]

This still exists? I thought this was going away a long time ago. @Yury G. Kudryashov didn't you have plans to do this?

[Kim Morrison]

Looking forward to it gone. :-)

[Yury G. Kudryashov]

I had plans but I have very little time for Mathlib these days.

[Yury G. Kudryashov]

In fact, since emultiplicity was ported to ENat, we can just drop the PartENat`.

[Yury G. Kudryashov]

I can try to do it tomorrow.

[Yury G. Kudryashov]

It looks like PartENat was deprecated ~2mo ago. The file is never imported by anything but Mathlib.lean. All the occurrences of PartENat in other files are in the docs.

[Yury G. Kudryashov]

Not sure how exactly should we deal with this deprecation.

[Yury G. Kudryashov]

#31529 removes PartENat from docs

[Ruben Van de Velde]

Would be good to update the documentation, but is there any reason to remove it in a hurry if it'll be removed at the 6 months mark?

[Yury G. Kudryashov]

Should we explicitly deprecate all defs and theorems in the file, or do you think that deprecating the type is enough?

[Ruben Van de Velde]

Either is fine, I think