付録をトップページに載せる

LeanByExample/EXTRA/README.lean

@@ -1,5 +1,9 @@
 /- # 付録
 
-`LeanByExample/EXTRA` 配下のページは、サイドバーの目次には掲載されません。
+付録です。以下のような用途で使います。
 
+* Lean の構文要素に対応しない話をする。
+* 各ページに載せるには少し長すぎる具体例を紹介する。
+* 用語の解説をする。
+* 数学の背景知識の解説をする。
 -/

LeanByExample/SUMMARY.lean

@@ -7,6 +7,17 @@
 [Mathlib4 Help](./Mathlib4Help.md)
 [ランダムページ](./Random.md)
 
+- [付録](./EXTRA/README.md)
+  - [カントールの定理](./EXTRA/Cantor.md)
+  - [クワイン](./EXTRA/Quine.md)
+  - [じゃんけんゲーム](./EXTRA/Janken.md)
+  - [三目並べ](./EXTRA/TicTacToe.md)
+  - [嫉妬深い夫たちの川渡りパズル](./EXTRA/Jealous.md)
+  - [選択ソート](./EXTRA/SelectionSort.md)
+  - [天使と悪魔の論理パズル](./EXTRA/AngelAndDevil.md)
+  - [末尾再帰](./EXTRA/TailRec.md)
+  - [列挙型に対する `ToString` インスタンスの自動生成](./EXTRA/EnumToString.md)
+
 ---
 
 - [対話的コマンド](./Diagnostic/README.md)
@@ -293,16 +304,4 @@
   - [show .. from: 項の型を明示](./Syntax/Show.md)
   - [Σ: 依存ペア型](./Syntax/Sigma.md)
 
-<!-- 以下は付録であり、サイドバーに表示されないことが期待される -->
-
-- [付録](./EXTRA/README.md)
-  - [選択ソート](./EXTRA/SelectionSort.md)
-  - [じゃんけんゲーム](./EXTRA/Janken.md)
-  - [３目並べ](./EXTRA/TicTacToe.md)
-  - [嫉妬深い夫たちの川渡りパズル](./EXTRA/Jealous.md)
-  - [天使と悪魔の論理パズル](./EXTRA/AngelAndDevil.md)
-  - [末尾再帰](./EXTRA/TailRec.md)
-  - [カントールの定理](./EXTRA/Cantor.md)
-  - [クワイン](./EXTRA/Quine.md)
-  - [列挙型に対する `ToString` インスタンスの自動生成](./EXTRA/EnumToString.md)
 -/

book.toml

@@ -25,16 +25,12 @@ additional-js = [
   "assets/replaceToLink.js",
   # ランダムページボタンを表示する
   "assets/randomPage.js",
-  # サイドバーに表示しないページを隠す
-  "assets/hiddenPages.js"
 ]
 additional-css = [
   # mdbook-admonish のスタイル
   "./assets/mdbook-admonish.css",
   # ページごとの目次をサイドバーとして表示する
   "./assets/pagetoc.css",
-  # サイドバーに表示しないページを初期描画から隠す
-  "./assets/hidden-pages.css",
 ]
 
 # セクション番号を振らない