Introduction and basic question

Stream: new members

[Rudolf Meijer]

Hello, I am Rudolf Meijer, interested in all kinds of programming languages and currently delving into functional programming. If I am going to use Lean, it will be for programming rather than theorem proving. My first question is: where do I find a list of all built-in functionality of Lean, e.g. what functions are available on Lists, of what type is the division of two Nat numbers, how do I print a value other than of String type, etc. etc. ?

[Kyle Miller]

For Lean 4, there's the auto-generated documentation at https://leanprover-community.github.io/mathlib4_docs/ that includes core Lean, the std library, and mathlib.

[Rudolf Meijer]

Thanks a lot. Those pages are much more readable than the source -- but I haven't seen a list of all operator signs and syntactic sugar that is also very handy to have, e.g. I thought I saw || and && somewhere, but what about :: and ++ etc.

[Kyle Miller]

In vscode you should be able to right click notation and "go to definition"

[Kyle Miller]

It'd be nice to have notation in the documentation, but as far as I know no ones done that yet.

[Rudolf Meijer]

I am on a simple text editor, alas, so I have to glean it from examples, I suppose. But the most urgent is to understand the difference between :: and ++.

[Kyle Miller]

I strongly suggest using VS Code if you're going to be using Lean 4. It's very difficult to use without interactive typechecking.

[Kyle Miller]

You can search for :: in the documentation and it links to something relevant

[Kyle Miller]

Here's what gives ++ notation for lists: https://github.com/leanprover/lean4/blob/fedf235cba35ed8bf6bf571cf38e6d8536b904ac/src/Init/Data/List/Basic.lean#L90

[Rudolf Meijer]

I spoke too soon, because in Init/Notation I found already a lot! I will work my way through for the moment. Thanks again for your rapid response, considering that you are in CA and I am in EU -- the time difference must be 9 or 10 hrs :-).

[Kyle Miller]

Oh, I'm in France right now, which helps with that (no need for the usual time traveling)

[Rudolf Meijer]

Right!

[Kyle Miller]

In case you aren't aware of it, there's Functional Programming in Lean

(Also, it does pain me to suggest VS Code. I generally use emacs, but the Lean plugins for VS Code seem to be better supported. One problem with using emacs is that it does not implement interactive "widgets" in the Lean goal view, which are useful for exploration of complicated types -- and implementing widgets for emacs would be a more significant undertaking than anyone's wanted to take on.)