--- tags: lean --- # Environment Setup 1. 裝 VSCode 的 `lean` extension 2. `lean` 及 `elan` 安裝完成後，在 terminal 下 ```sh $ elan default leanprover/lean4:nightly ```