Leanの環境構築
from Lean
docs
VSCodeの拡張を入れると自動で整うっぽいが、何か嫌だったのでnix経由でelanを入れた
入れた後に$ elan default stableが必要だった
めんどければplaygroundでも良さそう