3 ms·
As someone who has written a lot of Haskell in the past I would love to take a closer look at Lean (as a functional programming language rather than as a proof
by Herbstluft 4y ago
As someone who has written a lot of Haskell in the past I would love to take a closer look at Lean (as a functional programming language rather than as a proof assistant) but the documentation and information on that end seems very poor.
There's the manual [1] and "Functional programming in lean" [2] and they enabled me to get programming with it and solving some basic puzzles, but they are both WIP and unfinished.
I would love to explore Lean 4 more but with the current situation it's a bit too time consuming. Hope there will be more in the future.
[1]: https://leanprover.github.io/lean4/doc/ https://leanprover.github.io/lean4/doc/
[2]: https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/
- 7ewkVE6jJquN7e3 4y agoI strongly encourage you to check back in a couple of months. I expect things will be a lot more polished then. The team is currently quite busy with porting mathlib from Lean 3 to Lean 4. This is an excellent stress test for the language, and it's used to find and fix all sorts of minor bugs.
- Herbstluft 4y agoWill do! Certainly looking forward to it.
- dunham 4y agoI've been doing advent of code in Lean this year. It's been fun, but yeah the documentation is still a WIP. I've been searching the lean code base (I leave it in a separate editor window) and Zulip to figure out how to do stuff. The editor support is quite interesting, and the live updates of #eval statements have helped. I look forward to finding time to do a deeper dive into the language.