comment in Data/Set/Lattice

Stream: Is there code for X?

[Edison Xie]

in line 346 there is a comment saying -- classical, is that there on purpose or should that be deleted?

[Ruben Van de Velde]

It dates back to the first (technically second) commit of mathlib 3, but I don't see what it could mean, so it'd be fine to delete

[Andrew Yang]

It probably means “this lemma uses classical axioms”?

[Ruben Van de Velde]

I doubt it's the first in that file. Also line 308 and 312 should go

[Ruben Van de Velde]

(I can also pick it up in my next cleanup pr)

[Robin Carlier]

There is also a bunch of them starting from line 909. Also in Data/Set/Pairwise/Basic (lines 286, 311, 333). No other occurrences of -- classical within Mathlib.

[Yury G. Kudryashov]

I agree with @Andrew Yang above. I think that all these lines can be safely removed from the library.