_root_ を構文のカテゴリで見出し語にしない

Examples/Syntax/Namespace.lean

@@ -1,5 +1,4 @@
-/-
-# namespace
+/- # namespace
 `namespace` は，定義に階層構造を与えて整理するための構文です．名前空間 `Foo` の中で `bar` を定義すると，それは `Foo.bar` という名前になり，名前空間 `Foo` の中では短い名前 `bar` でアクセスできますが，名前空間を出るとアクセスにフルネームが必要になります．
 
 なおここでは説明のために `namespace` の中をインデントしていますが，これは一般的なコード規約ではありません．
@@ -41,3 +40,43 @@ namespace Nat
 end Nat
 
 #check Nat.Even.thirty
+
+/-
+## 名前空間を一時的に抜ける
+
+名前空間を一時的に抜けたいとき，`_root_` が使用できます．名前空間 `Hoge` の中で `foo` を定義すると `Hoge.foo` という名前になりますが，`_root_.foo` と定義すればこの挙動を避けて `foo` という名前にすることができます．
+
+たとえば以下のように名前空間の中で `List` 配下の関数を定義し，フィールド記法を使おうとしてもうまくいきません．こういう場合に `_root_` を使用すると，名前空間を閉じることなくエラーを解消できます．
+-/
+namespace Root -- 名前空間 `Root` の宣言
+
+variable {α : Type}
+
+def List.unpack (l : List (List α)) : List α :=
+  match l with
+  | [] => []
+  | x :: xs => x ++ unpack xs
+
+/--
+error: invalid field 'unpack', the environment does not contain 'List.unpack'
+  [[1, 2], [3]]
+has type
+  List (List Nat)
+-/
+#guard_msgs (whitespace := lax) in
+#check ([[1, 2], [3]] : List (List Nat)).unpack
+
+-- エラーになる原因は，名前空間 `Root` の中で宣言したので
+-- 関数名が `Root.List.unpack` になってしまっているから
+#check Root.List.unpack
+
+-- `_root_` を頭につけて再度定義する
+def _root_.List.unpack (l : List (List α)) : List α :=
+  match l with
+  | [] => []
+  | x :: xs => x ++ unpack xs
+
+-- 今度は成功する
+#eval [[1, 2], [3]].unpack
+
+end Root

src/SUMMARY.md

@@ -20,7 +20,6 @@
   - [#time: 実行時間計測](./DiagnosticCommand/Time.md)
 
 - [構文](./Syntax/README.md)
-  - [`_root_`: 一時的に名前空間を抜ける](./Syntax/Root.md)
   - [abbrev: 別名を定義する](./Syntax/Abbrev.md)
   - [attribute: 属性を付与する](./Syntax/Attribute.md)
   - [class: 型クラスを定義する](./Syntax/Class.md)