Type (max(maxu_3u_2)0) in docs

Stream: general

[Kevin Buzzard]

docs#FormalMultilinearSeries has type displayed as Type (max(maxu_3u_2)0) with no spaces in the docs (at least on my Firefox and Ubuntu). Is this a known issue?

[Niels Voss]

I have the same issue on Windows and Firefox. It seems to apply to any usage of max in universe levels, as PSum (α : Sort u) (β : Sort v) has type Sort (max(max1u)v). I think this applies to Chrome as well.

[Kyle Miller]

It shouldn't be browser-specific, you can see (max(maxu_3u_2)0) in the HTML