documentation

Stream: lean4

[J. O.]

does lean 4 have any documentation for its std?

[J. O.]

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

[Henrik Böving]

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]

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]

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.]

how about for lean

[J. O.]

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]

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]

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]

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

[J. O.]

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

[J. O.]

How do people learn all the functions provided in the std

[Henrik Böving]

They read the source code of the compiler / stdlib

[J. O.]

Henrik Böving said:

They read the source code of the compiler / stdlib

Oof, so there is no guide

[J. O.]

o wow

[Henrik Böving]

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.]

The std in the lean4 source code is very small

[J. O.]

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

[Henrik Böving]

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]

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

[J. O.]

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.]

in vscode?

[Arthur Paulino]

ctrl+click

[Arthur Paulino]

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

[J. O.]

hmm ok

[Arthur Paulino]

Reading those definitions has done wonders to my understanding

[J. O.]

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