Order.LocallyFinite !4#1754

Stream: mathlib4

[Ruben Van de Velde]

Anyone who wants to write some docstrings for this?

[Johan Commelin]

If the linter complains, just nolint.

[Johan Commelin]

That shouldn't hold up the port.

[Johan Commelin]

But please leave a Porting note. So that we don't forget about those nolints.

[Yaël Dillies]

I wrote the original file. I can write the docstrings tonight if you want.

[Ruben Van de Velde]

I pushed some not-great ones, feel free to suggest improvements on the PR

[Eric Wieser]

Isn't the right thing to do here to copy across the nolints.txt from lean3?

[Eric Wieser]

Because otherwise we are responsible for fixing every lint errors during the port

[Johan Commelin]

Yes, we should do that. But I don't know how hard it is to make it work.

[Ruben Van de Velde]

In this case, it was faster to write up some comments than figure out how to apply nolint attributes to class fields

[Eric Wieser]

nolints.txt is a different thing to the nolint attribute

[Eric Wieser]

Apparently in mathlib4 it's nolints.json