Lean4: Standard Library Documentation

Stream: new members

[awalterschulze]

I have read Theorem Proving in Lean4 and the Lean Manual and I am very impressed with the documentation. The only thing I can't find is some documentation and search for the Lean4 standard library, does this exist?

[Mario Carneiro]

docs4#Std.HashMap

[awalterschulze]

Perfect thank you :)

[awalterschulze]

We found that this documentation is slightly out of date. Is there an up to date version or a plan to up date https://leanprover.github.io/reference/libraries.html ?

[Kevin Buzzard]

You are the second person in a few hours to ask where the standard library is. Perhaps people don't want to update this page because they feel like the moment they point to the standard library they will have to write some overview saying what it is and what it does.

The standard library just appeared; it is here https://github.com/leanprover/std4 and right now you'll have to make do with the docs available online which are here https://leanprover-community.github.io/mathlib4_docs/Std/Data/Int/Basic.html#Int.sign . I don't know enough about Lean 4 to explain the difference between what is in core and what is in std4, beyond the assertion that what's in core is the bare minimum that is needed to get Lean up and running as a programming language and prover.

The mathematics library is in the process of being ported from Lean 3 to Lean 4. It's here https://github.com/leanprover-community/mathlib4 and you can find information about the Lean 3 version here https://leanprover-community.github.io/ , although much of what is explained there (e.g. about how much undergraduate mathematics is in the library) does not yet apply to mathlib4, although it will do one day.

[Henrik Böving]

That assertion is indeed the only difference.

[awalterschulze]

Okay, so the standard library has only recently been published, so we'll have to wait a bit for the documentation to also be updated and until then we can use the mathlib4 community docs or browse the source code.
Thank you everyone for answering my question.