Zulip Chat Archive

Stream: lean4

Topic: documentation


J. O. (Jan 24 2022 at 20:29):

does lean 4 have any documentation for its std?

J. O. (Jan 24 2022 at 20:29):

also, is lean 4's std even complete? does it have all the list functions that lean has?

Henrik Böving (Jan 24 2022 at 20:41):

The documentation is mostly the code, there is some WIP web doku here https://leanprover-community.github.io/mathlib4_docs/.

No the std lib is not complete, it does also at the moment not want to be complete since it is not an std lib in the traditional sence but rather the library that contains everything the compiler needs to bootstrap itself, the dumpster for "everything stdlib that doesnt belong into the compiler" is currently mathlib4.

Patrick Massot (Jan 24 2022 at 20:43):

Henrik, the first link I randomly tried was https://leanprover-community.github.io/mathlib4_docs/Init/Hints.html that is a bit disappointing. There isn't much in the Lean file either, but still something.

Henrik Böving (Jan 24 2022 at 20:45):

Yes currently everything that is a line file is getting linked, regardless of whether it actually has (renderable) content or not, This is also the first time I have ever seen the unif_hint keyword so I wouldn't know how to get the information to render it right now even :sweat_smile:. But I'll put it on the list!

J. O. (Jan 24 2022 at 20:46):

how about for lean

J. O. (Jan 24 2022 at 20:46):

does lean have a complete std and documentation? I like using methods like fold, sum, max, filter, map, but there are others which I need documentation for.

Henrik Böving (Jan 24 2022 at 20:48):

Are you referring to Lean 3? It's documentation state is basically the same, except that the doc-gen stuff for Lean 3 is of course much better fleshed out. What kind of documentation are you even looking for?

Henrik Böving (Jan 24 2022 at 20:50):

Patrick Massot said:

Henrik, the first link I randomly tried was https://leanprover-community.github.io/mathlib4_docs/Init/Hints.html that is a bit disappointing. There isn't much in the Lean file either, but still something.

https://github.com/leanprover/doc-gen4/issues/25

I'll be a little inactive on doc-gen until my exams are over in the next Thursday so you'll have to wait a bit :p

Patrick Massot (Jan 24 2022 at 20:51):

There is no hurry at all. Thank you very much for your work on this!

J. O. (Jan 24 2022 at 20:58):

How am I going to use lean with no documentation?!

J. O. (Jan 24 2022 at 20:58):

How do people learn all the functions provided in the std

Henrik Böving (Jan 24 2022 at 21:00):

They read the source code of the compiler / stdlib

J. O. (Jan 24 2022 at 21:00):

Henrik Böving said:

They read the source code of the compiler / stdlib

Oof, so there is no guide

J. O. (Jan 24 2022 at 21:00):

o wow

Henrik Böving (Jan 24 2022 at 21:02):

There is a little guide on how to do proofs and stuff. Regarding regular programming the best example and guide right now is definitely to read what's there already. I'd hope that this does change eventually but right now Mathlib4 is the focus.

J. O. (Jan 24 2022 at 21:03):

The std in the lean4 source code is very small

J. O. (Jan 24 2022 at 21:03):

so if im correct, lean 4 has no filter, map, fold, unfold, max, etc

Henrik Böving (Jan 24 2022 at 21:03):

Oh of course, but they are not in std they are defined in other packages and locations, you can find them by e.g. pressing go to definition on List.map

Henrik Böving (Jan 24 2022 at 21:04):

Lots of the stuff you are asking for will be in the Init package.

J. O. (Jan 24 2022 at 21:04):

Henrik Böving said:

Oh of course, but they are not in std they are defined in other packages and locations, you can find them by e.g. pressing go to definition on List.map

Where can i go to definition?

J. O. (Jan 24 2022 at 21:04):

in vscode?

Arthur Paulino (Jan 24 2022 at 21:04):

ctrl+click

Arthur Paulino (Jan 24 2022 at 21:05):

You can do #check List.map and ctrl+click on that

J. O. (Jan 24 2022 at 21:07):

hmm ok

Arthur Paulino (Jan 24 2022 at 21:08):

Reading those definitions has done wonders to my understanding

J. O. (Jan 24 2022 at 21:09):

this website is very useful: https://leanprover-community.github.io/mathlib4_docs/Init/Data/List/Basic.html


Last updated: Dec 20 2023 at 11:08 UTC