Zulip Chat Archive

Stream: general

Topic: quote mark in doc

Sebastien Gouezel (Sep 29 2020 at 14:06):

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 (Sep 29 2020 at 14:07):


Rob Lewis (Sep 29 2020 at 14:07):

There must be localized notation R somewhere?

Reid Barton (Sep 29 2020 at 14:07):

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

Patrick Massot (Sep 29 2020 at 14:07):

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

Patrick Massot (Sep 29 2020 at 14:08):

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 (Sep 29 2020 at 14:09):

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

Sebastien Gouezel (Sep 29 2020 at 14:11):

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 (Sep 29 2020 at 14:13):

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.

Last updated: Aug 03 2023 at 10:10 UTC