module と import¶
Lean のファイルは import 可能な単位として扱われます． import で使う module 名は，ソースルートからのパスに対応します．
たとえば次のように対応します．
LeanMathNote.lean module LeanMathNote
LeanMathNote/basic/chapter01.lean module LeanMathNote.basic.chapter01
LeanMathNote/basic/chapter06.lean module LeanMathNote.basic.chapter06
LeanMathNote/practice/chapter01.lean module LeanMathNote.practice.chapter01
別の module を使うには，ファイル冒頭で import します．
import Mathlib は Mathlib 全体を読み込むので講義資料では便利です．
実際の大きな開発では，ビルド時間を抑えるために必要な module だけを import します．
Lean Reference 最新版では，module header を使った module system のもとで，
public，private，import all，@[expose] などによって公開範囲や定義本体を展開できる範囲を制御する話も出てきます．
これは，ほかの module から名前を参照できるか，定義本体を unfolding できるか，変更時にどこまで再ビルドが必要になるかに関係します．
通常の Mathlib 利用やこの講義資料では，まず「ファイルパスと import 名の対応」と namespace の違いを理解すれば十分です．
namespace ModuleExample
def localDefinition : Nat :=
10
example : localDefinition = 10 := by
rfl
end ModuleExample
namespace は module とは別の仕組みです．
module はファイル単位の読み込み単位で，namespace は名前の階層を作る仕組みです．
同じ module の中に複数の namespace を置くことも，複数の module に同じ namespace の定義を分散させることもできます．