export
export
コマンドは、他の名前空間から定義を現在の名前空間に追加します。
具体的には、Some.Namespace
の配下に nameᵢ
がある状態で export Some.Namespace (name₁ name₂ ...)
を実行することにより、以下の両方の処理が行われます。
open
と同様に、nameᵢ
がSome.Namespace
の接頭辞なしで現在の名前空間N
上で見えるようになります。- 現在の名前空間
N
の外部の名前空間からN.nameᵢ
としてアクセスできるようになります。
namespace N -- export コマンドが実行される名前空間
inductive Sample : Type where
| foo
| bar
| baz
-- foo は名前空間 Sample 上にあるので、
-- 短い名前ではアクセスできない
#check_failure foo
#check Sample.foo
-- foo を現在の名前空間 N に追加する
export N.Sample (foo)
-- 短い名前でもアクセス可能になった
#check foo
end N
-- 名前空間 `N` の外部からアクセスするには、
-- 普通はフルネームが必要
#check_failure N.bar
#check N.Sample.bar
-- しかし foo は名前空間 N の内部で export されているので、
-- N を指定するだけでアクセス可能
#check N.foo