project の中で Lean ファイルを確認する¶
project の依存関係を使って 1 ファイルを確認したいときは，lake env lean を使います．
import Mathlib を含むファイルを素の lean MyProject/Basic.lean で実行すると，
Mathlib が見つからないことがあります．
lake env は，Lake workspace の依存関係を含む環境変数を設定したうえでコマンドを実行します．
この project なら，たとえば次のように章単体を確認できます．
前者はファイルパスで Lean を直接実行し，後者は Lake target として module をビルドします．