Mathlib を含まない project を作る

Mathlib を使わない最小 project は次で作れます．

lake new my_project
cd my_project
lake build

lake new my_project は，現在のディレクトリの下に my_project/ を作り，その中に Lake package を生成します． 生成される典型的な構成は次のようなものです．

my_project/
  lakefile.toml
  lean-toolchain
  MyProject.lean
  MyProject/
    Basic.lean

Lean の module 名はファイルパスに対応します． たとえば MyProject/Basic.lean は，通常 import MyProject.Basic で import できます．

lake init my_project という作り方もあります． これは，すでに存在する空ディレクトリの中で project を初期化したいときに使います．

mkdir my_project
cd my_project
lake init my_project