Floating point numbers

Stream: new members

[J. O.]

Where are the floating point numbers in lean?

[Adam Topaz]

docs#float

[Mario Carneiro]

there is docs#native.float for actual floats in the interpreter, and docs#fp.float is an (experimental) model of IEEE floats in mathlib

[J. O.]

Adam Topaz said:

docs#float

404 error and that is not lean 4

[Arthur Paulino]

@J. O. type #check Float and ctrl+click on Float. It will take you to its definition

[Arthur Paulino]

Unless you ask in #lean4 or explicitly say that you're asking about Lean 4, the common response will likely assume that you're asking about Lean 3

[J. O.]

Arthur Paulino said:

J. O. type #check Float and ctrl+click on Float. It will take you to its definition

So its a type? Why isn’t it in the manual. Or maybe it is

[Arthur Paulino]

You'll need to be a bit more patient for the Lean 4 manual :+1:

[Adam Topaz]

You can always look at the source
https://github.com/leanprover/lean4/blob/master/src/Init/Data/Float.lean

[Johan Commelin]

@J. O. Please, in this thread you are interacting with volunteers that are trying to be helpful. Recently you've been coming across quite negatively or dismissive. Lean 4 is not a polished product. Lean 3 is a community maintained project. We aren't selling anything. We're trying out tons of things, and doing experiments that have never been done before. Most of what's going on is like construction workers on a construction site. And since most of us are those "construction workers", we really enjoy being at the construction site.
I encourage you to be more kind in what you write.

[Johan Commelin]

Note that https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Chapters.20that.20make.20no.20sense/near/270140494 is flagged with :butterfly: by several people.

[Johan Commelin]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Community.20Guidelines/near/235207529 for explanation of the :butterfly:

[J. O.]

Johan Commelin said:

J. O. Please, in this thread you are interacting with volunteers that are trying to be helpful. Recently you've been coming across quite negatively or dismissive. Lean 4 is not a polished product. Lean 3 is a community maintained project. We aren't selling anything. We're trying out tons of things, and doing experiments that have never been done before. Most of what's going on is like construction workers on a construction site. And since most of us are those "construction workers", we really enjoy being at the construction site.
I encourage you to be more kind in what you write.

Sorry