Where is Float?

Stream: new members

[mars0i]

Sometimes I look go looking for functions and types by using the menu of libraries at the left in the documentation. I couldn't find Float, and found it using the search function, but where is it? I don't see it in Init.Data or Lean.Data, which are two places I expected to find it. It's not in Mathlib.Data.

[Edward van de Meent]

docs#Float suggests it is in Init.Data

[Edward van de Meent]

(but in a subdirectory)

[mars0i]

Thanks. I had looked in Init.Data on the left side of the docs, but overlooked the Float entry. (I looked repeatedly; don't know how I missed it.)

[Kyle Miller]

Tip: the left side bar unfolds when you do a ctrl-f search.

[mars0i]

What browser do you use, @Kyle Miller? Sounds nice. MacOS Firefox doesn't do it.

[Kyle Miller]

Chrome