Mathlib docs le vs lt

Stream: general

[Ryan Lahfa]

I use often mathlib docs and found really difficult to read le vs lt theorems, due to the fact they're most of the time links themselves, so they get underlined and it can get confusing with the "underline" of le ≤

Would it be interesting I do a PR to the CSS of doc-gen so we can get rid of this? Or is there a better alternative?

[Johan Commelin]

Hmm, yeah, that sounds like it's worth a PR

[Johan Commelin]

Maybe only underline on hover...

[Alex J. Best]

Or a lighter underline colour?

[Ryan Lahfa]

Guess it depends, those links are not even redirecting to some page, they're only anchor so we can refer to the location of something. But, we can also just use theorem as anchors and not part of the theorem as anchors, right?

[Johan Commelin]

Yeah, makes sense.

[Johan Commelin]

But @Rob Lewis is the boss of the docs pages (-;

[Ryan Lahfa]

I've done it locally using Stylish and local CSS for me. Here's it looks like. DeepinScreenshot_select-area_20200323204032.png

[Ryan Lahfa]

It's hacky and dirty but can be reproduced with those rules injected in the stylesheet:

.decl_type a:link, .structure_field a:link {
    text-decoration: none !important;
}

.decl_type a:hover, .structure_field a:hover {
    text-decoration: underline !important;
}

[Patrick Massot]

I always said there are too many underlines in this CSS. Basically every word is underlined, this is clearly pointless.

[Ryan Lahfa]

Patrick Massot said:

I always said there are too many underlines in this CSS. Basically every word is underlined, this is clearly pointless.

Definitely, the only underline which "makes sense" to me is when we underline theorem or lemmas names so we can refer to them easily and pass a link. Otherwise, it's killing my eyes each time I try to find out if this is a ≤ or < especially in structure fields.

[Rob Lewis]

Ryan Lahfa said:

Guess it depends, those links are not even redirecting to some page, they're only anchor so we can refer to the location of something. But, we can also just use theorem as anchors and not part of the theorem as anchors, right?

I'm not sure I follow. Clicking on < should direct you to the entry for has_lt.lt. In general, clicking on any name (or notation) that appears in a type should direct you to the entry for that name. I don't like removing the underlines entirely, since then it's not clear that things are clickable at all.

[Rob Lewis]

That said, I see that < and ≤ are hard to distinguish.

[Rob Lewis]

Maybe changing the color or weight of the underline would help.

[Patrick Massot]

I think we can clearly explain once and for all that everything is clickable.

[Ryan Lahfa]

Patrick Massot said:

I think we can clearly explain once and for all that everything is clickable.

I agree with this solution rather, when I hover on it, I can see it being underlined and I understand I can click it.
But I spend too much time trying to distinguish between < and ≤ in theorems involving those two at multiple places…

[Ryan Lahfa]

Rob Lewis said:

Ryan Lahfa said:

Guess it depends, those links are not even redirecting to some page, they're only anchor so we can refer to the location of something. But, we can also just use theorem as anchors and not part of the theorem as anchors, right?

I'm not sure I follow. Clicking on < should direct you to the entry for has_lt.lt. In general, clicking on any name (or notation) that appears in a type should direct you to the entry for that name. I don't like removing the underlines entirely, since then it's not clear that things are clickable at all.

Indeed, I misunderstood something.

The code I provided make them appear on hover, but even if we change the color, it's going to be the same thing, it'll pollute the visual overview of a theorem :/.

I think it'd be better to adopt another way, but it cannot be at foreground, it must be at background so it does not collision with mathematical symbols, e.g. = becomes \equiv visually with underlines.