diff --git a/Src/Private.lean b/Src/Private.lean new file mode 100644 index 0000000..67c34bf --- /dev/null +++ b/Src/Private.lean @@ -0,0 +1,19 @@ +/- # private +`private` は,その定義があるファイルの中でだけ参照可能になるようにする修飾子です. + +不安定なAPIなど,外部に公開したくないものに対して使うのが主な用途です. + +なお `private` コマンドでセクションや名前空間にスコープを制限することはできません. +-/ + +namespace Hoge + section + -- private とマークした定義 + private def addOne (n : Nat) : Nat := n + 1 + end +end Hoge + +open Hoge + +-- アクセスできる +#check addOne diff --git a/md/SUMMARY.md b/md/SUMMARY.md index f560c17..d614206 100644 --- a/md/SUMMARY.md +++ b/md/SUMMARY.md @@ -15,7 +15,7 @@ * [instance: インスタンスを定義する]() * [namespace: 定義を階層化する](./build/Namespace.md) * [open: 名前空間を開く](./build/Open.md) -* [private: 定義を不可視にする]() +* [private: 定義を不可視にする](./build/Private.md) * [protected: フルネームを強制する](./build/Protected.md) * [section: 引数のスコープを区切る](./build/Section.md) * [structure: 構造体を定義する](./build/Structure.md)