Search in published documentation

Stream: mathlib4

[Stephan Maier]

Using the published documenation at
https://leanprover-community.github.io/mathlib4_docs/
I discovered that the search is case-sensitive. When searching, e.g. for "CoAlgebra" the result-list does not even list anything that has "coalgebra" in its name. When searching for "Coalgebra" one finds a plethora of results. Is case-sensitivity a conscious choice, or would it be an improvement no to be case-sensitive (I prefer abandoning case-sensitivity).
Thanks for all the great work! I am quite impressed!

[Richard Osborn]

The search function is only case-sensitive when searching with uppercase letters, afaik. "Coalgebra" will look for an uppercase "C" but will ignore the case for all the other characters. "coalgebra" is entirely case-insensitive (i.e. it will find "Coalgebra" as well)

[Kevin Buzzard]

Related: I discovered that the search is not case-sensitive. Indeed, someone used sigma in some code, but didn't mention an earlier open, and I wanted to know which sigma it was so I searched the docs for sigma and the answer I wanted to see (docs#ArithmeticFunction.sigma) didn't even show up in the docs search popup because it was dominated by all the Sigmas (which I knew I didn't want).

sigma.png

[Richard Osborn]

Perhaps the search could allow using quotes to denote case-sensitivity (search with "sigma" instead of sigma).

[Stephan Maier]

Richard Osborn said:

The search function is only case-sensitive when searching with uppercase letters, afaik. "Coalgebra" will look for an uppercase "C" but will ignore the case for all the other characters. "coalgebra" is entirely case-insensitive (i.e. it will find "Coalgebra" as well)

Thanks for the hint, it helps greatly!