21–30 of 152 posts
>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension, Lol
- Emacs: https://github.com/leanprover-community/lean4-mode
- Neovim: https://github.com/Julian/lean.nvim
I'm using the Emacs lean4-mode and it's pretty good.
wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
Wow, I read the whole thing without noticing that. But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.
if you wanted more than one sentence you sent one then wrote the other
it's painful to read longform
the victorians didn't give up on punctuation and regular english just because they had the telegraph
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only heard about lean through HN posts.
The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.
[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ (Cedar)
Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore. Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad. Personally, I…
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.