namespace と open¶
namespace は，名前を整理するためのコマンドです．
大きなプロジェクトでは，同じような名前の定義がたくさん出てきます．
名前空間を使うと，Geometry.Point のように，どの分野・モジュールの名前かを明示できます．
namespace Geometry
structure Point where
x : Int
y : Int
deriving Repr, DecidableEq
def origin : Point :=
{ x := 0, y := 0 }
def reflectX (p : Point) : Point :=
{ x := p.x, y := -p.y }
example : reflectX origin = origin := by
rfl
end Geometry
名前空間の外から参照するときは，完全な名前 Geometry.Point や Geometry.origin を使います．
このファイル全体は namespace Chapter02 の中にあるので，厳密な完全名は Chapter02.Geometry.Point です．
ただし，同じ Chapter02 名前空間の中では Geometry.Point と書けます．
example : Geometry.Point :=
Geometry.origin
example : Geometry.reflectX Geometry.origin = Geometry.origin := by
rfl
open は，名前空間の中の名前を短く使えるようにするコマンドです．
open Geometry と書くと，そのスコープ内では Geometry.Point を Point，Geometry.origin を origin と書けます．
ただし，読み手にとって由来が分かりにくくなることもあるので，必要な範囲に限定して使うのがよいです．
section OpenExamples
open Geometry
def reflectedOrigin : Point :=
reflectX origin
example : reflectedOrigin = origin := by
rfl
end OpenExamples
namespace ... end は新しい名前空間に入る構文で，そこで定義した名前はその名前空間に属します．
一方，open は既存の名前空間を開いて，名前を短く参照するための構文です．
つまり，namespace は名前を作る場所を決め，open は名前を読むときの省略を許す，と考えるとよいです．
演習¶
namespace を使って，同じ名前の定義が衝突しないことを確認してください．