elan
インストール
macOS
$ brew install elan-init
$ elan default leanprover/lean4:stable
使い方
-V: バージョン情報
$ elan -V
$ elan show
$ elan default stable
mathlib4を使えるようにする
既存のプロジェクトの場合
lakefile.leanに下記を追加
code:memo
require mathlib from git
メモ
leanmake
leanproject
leanpkg
関連