Source code:
Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.
From CLI:
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env
Then when you run:
lean
it downloads the lean executable for you. Insane shit, could only come from a Microsoft mindset.
This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.
This used to have the best name ever allowing you to say:to English speakers and watch their faces drop.
But in 2023 the bastards renamed it to "Rocq", presumably pronounced "rock". Why, God, why.
This will never work but OK. New custom language after Lean.
It seems to implement Zermelo-Fraenkel set theory.

Articles by others on the same topic (0)

There are currently no matching articles.