open
open
は名前空間を開くためのコマンドです。
名前空間 N
の中にある定義 S
を使いたいとき、通常はフルネームの N.S
を使う必要がありますが、open N
とすることで短い別名 S
でアクセスできるようになります。
namespace Hoge
def foo := "hello"
end Hoge
-- 名前空間の外からだと `foo` という短い名前が使えない
#check_failure foo
section
-- 名前空間 `Hoge` をオープン
open Hoge
-- `open` することで `foo` という短い名前が使えるようになる
#check foo
end
-- セクションが終わると再び短い名前は使えなくなる
#check_failure foo
入れ子になった名前空間
名前空間 N₁
と N₂
が入れ子になっているとき、その下にある定義に短い名前でアクセスするには、open N₁ N₂
とすればよいです。
namespace Foo
namespace Bar
def baz := "world"
end Bar
end Foo
-- 入れ子の名前空間を開く
-- `Foo` の後に `Bar` を開く必要がある
open Foo Bar
#check baz
名前空間と公理
また名前空間 Foo
内に bar
という公理(axiom
で宣言されたもの)が存在する場合、Foo
を開くと同時に公理 Foo.bar
もインポートされます。
open Classical
-- 選択原理
#print choice
variable (P : Prop)
-- 選択原理が仮定された状態になっているため、
-- 任意の命題が決定可能になっている
#synth Decidable P