4 ms·

See also the Lean Game Server at https://adam.math.hhu.de/ https://adam.math.hhu.de/ , and in particular the "Natural Number Game" (for Lean 4!), which has done

by jml7c5 3y ago

See also the Lean Game Server at https://adam.math.hhu.de/ https://adam.math.hhu.de/ , and in particular the "Natural Number Game" (for Lean 4!), which has done the rounds on HN a few times. Does anyone know of a Lean book that builds up the basics from absolutely nothing, not even the Lean standard library? I'm curious about the foundations that lie just above the language.

ykonstant 3y ago
Your best bet lies with the introductory Functional Programming in Lean: https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/
crvdgc 3y ago
For me, the best route is to start with Functional Programming in Lean [1]. Get familiar with dependent type theory and Lean's syntax. Then go back to Lean's source code [2]. Lean is self-hosted, so the language is written in Lean. And it's well documented. Starting from the Prelude [3], all the way up to the language server (yes, Lean ships a parser combinator library and a JSON library with the language). One caveat is that the toolchain version of the repo is the repo itself, so you'd have to follow the development guide [4] to set it up. Also, this is different from the standard library std4 [5], which is actually not shipped with the language, but just a normal package developed and used as the standard library. [1]: https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/ [2]: https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 [3]: https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean https://github.com/leanprover/lean4/blob/master/src/Init/Pre... [4]: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md https://github.com/leanprover/lean4/blob/master/doc/dev/inde... [5]: https://github.com/leanprover/std4 https://github.com/leanprover/std4

by jml7c5 3y ago

ykonstant 3y ago

Your best bet lies with the introductory Functional Programming in Lean: https://lean-lang.org/functional_programming_in_lean/ https://lean-lang.org/functional_programming_in_lean/

crvdgc 3y ago

For me, the best route is to start with Functional Programming in Lean [1]. Get familiar with dependent type theory and Lean's syntax. Then go back to Lean's source code [2]. Lean is self-hosted, so the language is written in Lean. And it's well documented. Starting from the Prelude [3], all the way up to the language server (yes, Lean ships a parser combinator library and a JSON library with the language). One caveat is that the toolchain version of the repo is the repo itself, so you'd have to follow the development guide [4] to set it up. Also, this is different from the standard library std4 [5], which is actually not shipped with the language, but just a normal package developed and used as the standard library. [1]: https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/ [2]: https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 [3]: https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean https://github.com/leanprover/lean4/blob/master/src/Init/Pre... [4]: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md https://github.com/leanprover/lean4/blob/master/doc/dev/inde... [5]: https://github.com/leanprover/std4 https://github.com/leanprover/std4