private を追加する

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

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)