protected
protected
は、ある名前空間 Hoge
にある定義 foo
に対して、必ずフルネームの Hoge.foo
でアクセスすることを強要するものです。
structure Point where
x : Nat
y : Nat
namespace Point
protected def sub (p q : Point) : Point :=
{ x := p.x - q.x, y := p.y - q.y }
-- private のテスト用の宣言
private def private_sub := Point.sub
-- 名前空間の中にいても、短い名前ではアクセスできない
#check_failure sub
-- フルネームならアクセスできる
#check Point.sub
end Point
open Point
-- 名前空間を開いていても、短い名前でアクセスできない
#check_failure sub
-- フルネームならアクセスできる
#check Point.sub
protected を使う場面
環境の中に Foo.bar
と bar
が存在したとします。このとき名前空間 Foo
の中にいた場合は、Foo.bar
の方が優先されます。したがってルートにある方の bar
は覆い隠され、アクセスしづらくなります。
def Foo.bar := "hello"
def bar := "world"
namespace Foo
-- 単に bar と書くと Foo.bar が参照される
#guard bar = "hello"
-- ルートにある bar を参照することも _root_ を付ければ可能
#guard _root_.bar = "world"
end Foo
Foo.baz
を protected
として宣言しておけば、他の名前空間に影響を及ぼさなくなります。
protected def Foo.baz := "hello"
def baz := "world"
namespace Foo
-- 単に baz と書いたらルートの baz が参照される
#guard baz = "world"
end Foo
protected def 以外の用法
def
コマンドに対してだけでなく、indudctive
コマンドで生成されるコンストラクタに対しても使用可能です。
/-- 2分木 -/
inductive BinTree (α : Type) where
| empty : BinTree α
| protected node : α → BinTree α → BinTree α → BinTree α
-- 名前空間を開く
open BinTree
-- 名前空間を開いているのに、
-- コンストラクタに短い名前でアクセスできない
#check_failure node
#check BinTree.node
-- protected でない方は短い名前でアクセスできる
#check empty
また structure
コマンドで生成されるアクセサ関数やコンストラクタに対しても使用可能です。
structure Sample where
-- コンストラクタも protected にできる
protected mk ::
bar : Nat
protected hoge : String
open Sample
-- 名前空間を開いているので bar には短い名前でアクセスできる
#check bar
-- hoge には短い名前でアクセスできない
#check_failure hoge