Zulip Chat Archive

Stream: new members

Topic: Floating point numbers


J. O. (Feb 01 2022 at 01:51):

Where are the floating point numbers in lean?

Adam Topaz (Feb 01 2022 at 02:22):

docs#float

Mario Carneiro (Feb 01 2022 at 02:24):

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. (Feb 01 2022 at 03:00):

Adam Topaz said:

docs#float

404 error and that is not lean 4

Arthur Paulino (Feb 01 2022 at 03:06):

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

Arthur Paulino (Feb 01 2022 at 03:09):

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. (Feb 01 2022 at 03:16):

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 (Feb 01 2022 at 03:33):

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

Adam Topaz (Feb 01 2022 at 05:14):

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

Johan Commelin (Feb 01 2022 at 06:12):

@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 (Feb 01 2022 at 06:13):

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 (Feb 01 2022 at 06:17):

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

J. O. (Feb 01 2022 at 12:02):

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


Last updated: Dec 20 2023 at 11:08 UTC