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.
Comments
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/
[2]: https://github.com/leanprover/lean4
[3]: https://github.com/leanprover/lean4/blob/master/src/Init/Pre...
[4]: https://github.com/leanprover/lean4/blob/master/doc/dev/inde...
[5]: https://github.com/leanprover/std4