doc: hypotheses with ZMod

Stream: mathlib4

[Ralf Stephan]

In the mathlib web documentation, it seems that hypotheses containing ZMod are not shown. Is this intentional?

Example, compare with source: https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.html#ZMod.exists_sq_eq_two_iff

[Ralf Stephan]

In other words, (2 : ZMod p) is printed as 2.

[Ruben Van de Velde]

Nothing specific about ZMod here; it's just that the pretty printed output of a lean term is (unfortunately) not guaranteed to parse into the same term

[Ralf Stephan]

In VScode, at least I can hover over 2 and see what it is, but not on the doc pages. Should I submit a feature request?

[Kim Morrison]

I think the answer here is to wait for Verso to roll out further.