quote mark in doc

Stream: general

[Sebastien Gouezel]

In docs#continuous_linear_map (and everywhere else in this file), there are weird quotation marks around R at several places. Is this a new feature of the doc generator?

[Rob Lewis]

:sad:

[Rob Lewis]

There must be localized notation R somewhere?

[Reid Barton]

src/geometry/algebra/lie_group.lean:localized "notation `R` := right_mul" in lie_group

[Patrick Massot]

This certainly looks like an unwanted side effect of the recent nice notation work.

[Patrick Massot]

If this is currently the only such problem then the easiest work around is probably to (hopefully temporarily) get rid of this notation.

[Rob Lewis]

People should definitely keep an eye out for other bad consequences of the new feature.

[Sebastien Gouezel]

I'd like to stress that I find the doc website generally awesome. Hearing people complain when something is not perfect is useful, but saying when things are awesome is also useful I think :)

[Rob Lewis]

I think L and R aren't good notations even localized. This error could have shown up in a file that innocently opened that notation and had a type called R and it would have been way harder to debug.