Zulip Chat Archive

Stream: maths

Topic: Old docs


Heather Macbeth (Jul 25 2022 at 18:15):

Is there a way to see a past version of the docs?

I just noticed that the notation conj for star_ring_end ℂ is not displaying at, e.g., docs#inner_product_space.is_self_adjoint_iff_inner_map_self_real, but I thought that it used to display. I wonder if something has changed.

Eric Wieser (Jul 25 2022 at 20:12):

I mentioned this elsewhere, I think it's a regression in doc-gen

Eric Wieser (Jul 25 2022 at 20:14):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/doc-gen.20not.20showing.20sum.20notation


Last updated: Dec 20 2023 at 11:08 UTC